Showing 1–26 of 26 results for author: Goré, R

A Relevance Model for Threat-Centric Ranking of Cybersecurity Vulnerabilities

Authors: Corren McCoy, Ross Gore, Michael L. Nelson, Michele C. Weigle

Abstract: The relentless process of tracking and remediating vulnerabilities is a top concern for cybersecurity professionals. The key challenge is trying to identify a remediation scheme specific to in-house, organizational objectives. Without a strategy, the result is a patchwork of fixes applied to a tide of vulnerabilities, any one of which could be the point of failure in an otherwise formidable defens… ▽ More The relentless process of tracking and remediating vulnerabilities is a top concern for cybersecurity professionals. The key challenge is trying to identify a remediation scheme specific to in-house, organizational objectives. Without a strategy, the result is a patchwork of fixes applied to a tide of vulnerabilities, any one of which could be the point of failure in an otherwise formidable defense. Given that few vulnerabilities are a focus of real-world attacks, a practical remediation strategy is to identify vulnerabilities likely to be exploited and focus efforts towards remediating those vulnerabilities first. The goal of this research is to demonstrate that aggregating and synthesizing readily accessible, public data sources to provide personalized, automated recommendations for organizations to prioritize their vulnerability management strategy will offer significant improvements over using the Common Vulnerability Scoring System (CVSS). We provide a framework for vulnerability management specifically focused on mitigating threats using adversary criteria derived from MITRE ATT&CK. We test our approach by identifying vulnerabilities in software associated with six universities and four government facilities. Ranking policy performance is measured using the Normalized Discounted Cumulative Gain (nDCG). Our results show an average 71.5% - 91.3% improvement towards the identification of vulnerabilities likely to be targeted and exploited by cyber threat actors. The return on investment (ROI) of patching using our policies results in a savings of 23.3% - 25.5% in annualized costs. Our results demonstrate the efficacy of creating knowledge graphs to link large data sets to facilitate semantic queries and create data-driven, flexible ranking policies. △ Less

Submitted 9 June, 2024; originally announced June 2024.

Comments: 24 pages, 8 figures, 14 tables

ACM Class: K.6.5

GPT-4 Generated Narratives of Life Events using a Structured Narrative Prompt: A Validation Study

Authors: Christopher J. Lynch, Erik Jensen, Madison H. Munro, Virginia Zamponi, Joseph Martinez, Kevin O'Brien, Brandon Feldhaus, Katherine Smith, Ann Marie Reinhold, Ross Gore

Abstract: Large Language Models (LLMs) play a pivotal role in generating vast arrays of narratives, facilitating a systematic exploration of their effectiveness for communicating life events in narrative form. In this study, we employ a zero-shot structured narrative prompt to generate 24,000 narratives using OpenAI's GPT-4. From this dataset, we manually classify 2,880 narratives and evaluate their validit… ▽ More Large Language Models (LLMs) play a pivotal role in generating vast arrays of narratives, facilitating a systematic exploration of their effectiveness for communicating life events in narrative form. In this study, we employ a zero-shot structured narrative prompt to generate 24,000 narratives using OpenAI's GPT-4. From this dataset, we manually classify 2,880 narratives and evaluate their validity in conveying birth, death, hiring, and firing events. Remarkably, 87.43% of the narratives sufficiently convey the intention of the structured prompt. To automate the identification of valid and invalid narratives, we train and validate nine Machine Learning models on the classified datasets. Leveraging these models, we extend our analysis to predict the classifications of the remaining 21,120 narratives. All the ML models excelled at classifying valid narratives as valid, but experienced challenges at simultaneously classifying invalid narratives as invalid. Our findings not only advance the study of LLM capabilities, limitations, and validity but also offer practical insights for narrative generation and natural language processing applications. △ Less

Submitted 12 July, 2024; v1 submitted 8 February, 2024; originally announced February 2024.

Comments: 29 pages, 24 figures

ACM Class: I.2.7; I.6.4

Estimating Diffusion Degree on Graph Streams

Authors: Vinit Ramesh Gore, Suman Kundu, Anggy Eka Pratiwi

Abstract: The challenges of graph stream algorithms are twofold. First, each edge needs to be processed only once, and second, it needs to work on highly constrained memory. Diffusion degree is a measure of node centrality that can be calculated (for all nodes) trivially for static graphs using a single Breadth-First Search (BFS). However, kee** track of the Diffusion Degree in a graph stream is nontrivia… ▽ More The challenges of graph stream algorithms are twofold. First, each edge needs to be processed only once, and second, it needs to work on highly constrained memory. Diffusion degree is a measure of node centrality that can be calculated (for all nodes) trivially for static graphs using a single Breadth-First Search (BFS). However, kee** track of the Diffusion Degree in a graph stream is nontrivial. The memory requirement for exact calculation is equivalent to kee** the whole graph in memory. The present paper proposes an estimator (or sketch) of diffusion degree for graph streams. We prove the correctness of the proposed sketch and the upper bound of the estimated error. Given $ε, δ\in (0,1)$, we achieve error below $ε(b_u-a_u)d_uλ$ in node $u$ with probability $1-δ$ by utilizing $O(n\frac1{ε^2}\log{\frac1δ})$ space, where $b_u$ and $a_u$ are the maximum and minimum degrees of neighbors of $u$, $λ$ is diffusion probability, and $d_u$ is the degree of node $u$. With the help of this sketch, we propose an algorithm to extract the top-$k$ influencing nodes in the graph stream. Comparative experiments show that the spread of top-$k$ nodes by the proposed graph stream algorithm is equivalent to or better than the spread of top-$k$ nodes extracted by the exact algorithm. △ Less

Submitted 31 January, 2024; originally announced January 2024.

A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised

Authors: Ian Shillito, Iris van der Giessen, Rajeev Goré, Rosalie Iemhoff

Abstract: We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direc… ▽ More We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong Löb logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direct way, leading to a straightforward cut-elimination procedure. All proofs have been formalised in the interactive theorem prover Coq. △ Less

Submitted 1 September, 2023; originally announced September 2023.

Comments: 21-page conference paper + 4-page appendix with proofs

ACM Class: F.4.1

Analysis of Fault Tolerant Multi-stage Switch Architecture for TSN

Authors: Adnan Ghaderi, Rahul Nandkumar Gore

Abstract: We conducted the feasibility analysis of utilizing a highly available multi-stage architecture for TSN switches used for sending high priority, mission-critical traffic within a bounded latency instead of traditional single-stage architectures. To verify the TSN functionality, we implemented the 'strict priority' feature. We evaluated the performance of both architectures on multiple parameters su… ▽ More We conducted the feasibility analysis of utilizing a highly available multi-stage architecture for TSN switches used for sending high priority, mission-critical traffic within a bounded latency instead of traditional single-stage architectures. To verify the TSN functionality, we implemented the 'strict priority' feature. We evaluated the performance of both architectures on multiple parameters such as fault tolerance, packet latency, throughput, reliability, path length effectiveness, and cost per unit. The fault tolerance analysis demonstrated that the multi-stage architecture fairs better than the single-stage counterpart. The average latency and throughput performance of multi-stage architectures, although low, can be considered comparable with single-stage counterparts. However, the multi-stage architecture fails to meet the performance of single-stage architectures on parameters such as reliability, path length effectiveness, and cost-effectiveness. The improved fault tolerance comes at the cost of increased hardware resources, cost, and complexity. However, with the advent of cost-effective technologies in hardware design and efficient architecture designs, the multi-stage switching architecture-based TSN switches can be made reasonably comparable to single-stage switching TSN switches. This work gives initial confidence that the multi-stage architecture can be pursued further for safety-critical systems that require determinism and reliability in the communication of critical messages. △ Less

Submitted 23 September, 2022; originally announced September 2022.

N-PAT: A Nested Model-Checker

Authors: Hadrien Bride, Cheng-Hao Cai, ** Song Dong, Rajeev Gore, Zhé Hóu, Brendan Mahony, Jim McCarthy

Abstract: N-PAT is a new model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security ca… ▽ More N-PAT is a new model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security case study. △ Less

Submitted 11 May, 2020; originally announced May 2020.

Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents

Authors: Tim Lyon, Alwen Tiu, Rajeev Goré, Ranald Clouston

Abstract: We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all bee… ▽ More We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants. △ Less

Submitted 14 June, 2023; v1 submitted 11 October, 2019; originally announced October 2019.

Comments: Appended version of the paper "Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents", accepted to the 28th International Conference on Computer Science Logic (CSL 2020)

Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)

Authors: Rajeev Goré, Björn Lellmann

Abstract: We give a linear nested sequent calculus for the basic normal tense logic Kt. We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut-elimination. Linear nested sequents thus provide the minimal amount of nesting necessary to provide an adequate proof-theory for modal logics containing converse. As a bonus, this yields a cut-free calculus for symmetri… ▽ More We give a linear nested sequent calculus for the basic normal tense logic Kt. We show that the calculus enables backwards proof-search, counter-model construction and syntactic cut-elimination. Linear nested sequents thus provide the minimal amount of nesting necessary to provide an adequate proof-theory for modal logics containing converse. As a bonus, this yields a cut-free calculus for symmetric modal logic KB. △ Less

Submitted 2 July, 2019; originally announced July 2019.

Comments: Extended version of the paper accepted at TABLEAUX2019, containing an additional technical appendix

A Novel Hierarchical Circuit LUT Model for SOI Technology for Rapid Prototy**

Authors: Sitansusekhar Roymohapatra, Ganesh R. Gore, Akanksha Yadav, Mahesh B. Patil, Krishnan S. Rengarajan, Subhramanian S. Iyer, Maryam Shojaei Baghini

Abstract: This article is withdrawn because the co-authors are not in favor of publication. This article is withdrawn because the co-authors are not in favor of publication. △ Less

Submitted 26 April, 2019; v1 submitted 27 March, 2019; originally announced March 2019.

Comments: This article was uploaded by mistake without taking consent of co-authors including my Ph.D. guide. The co-authors are not in favor of publication of this article in arXiv. Hence I am withdrawing it. This is my mistake and I apologize for this

A case study in formal verification of a Java program

Authors: Dmitry Brizhinev, Rajeev Goré

Abstract: We describe a successful attempt to formally verify a simple genetic algorithm written in Java. To this end, we compare several formal verification tools designed for Java, and select Krakatoa as the most appropriate for the task. Based on our experience, we present several suggestions for making the tools more user friendly, which we hope will lead to wider adoption of formal methods. In particul… ▽ More We describe a successful attempt to formally verify a simple genetic algorithm written in Java. To this end, we compare several formal verification tools designed for Java, and select Krakatoa as the most appropriate for the task. Based on our experience, we present several suggestions for making the tools more user friendly, which we hope will lead to wider adoption of formal methods. In particular, we discuss at length how useful it would be for provers to perform some form of abduction, that is, for them to guess which extra assumptions they need to prove a statement. It is our opinion that progress in this area would produce the largest improvement in the usability of formal verification tools. △ Less

Submitted 10 September, 2018; originally announced September 2018.

Comments: Written in August 2016

Modular Labelled Sequent Calculi for Abstract Separation Logics

Authors: Zhé Hóu, Ranald Clouston, Rajeev Goré, Alwen Tiu

Abstract: Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are "abstract" because they are independent of any particular concrete resource model. Their assertion languages, called propositional abstract separation logics (PASLs), extend the logic of (Boolean) Bunched Implications (BBI) in variou… ▽ More Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are "abstract" because they are independent of any particular concrete resource model. Their assertion languages, called propositional abstract separation logics (PASLs), extend the logic of (Boolean) Bunched Implications (BBI) in various ways. In particular, these logics contain the connectives $*$ and $-\!*$, denoting the composition and extension of resources respectively. This added expressive power comes at a price since the resulting logics are all undecidable. Given their wide applicability, even a semi-decision procedure for these logics is desirable. Although several PASLs and their relationships with BBI are discussed in the literature, the proof theory and automated reasoning for these logics were open problems solved by the conference version of this paper, which developed a modular proof theory for various PASLs using cut-free labelled sequent calculi. This paper non-trivially improves upon this previous work by giving a general framework of calculi on which any new axiom in the logic satisfying a certain form corresponds to an inference rule in our framework, and the completeness proof is generalised to consider such axioms. Our base calculus handles Calcagno et al.'s original logic of separation algebras by adding sound rules for partial-determinism and cancellativity, while preserving cut-elimination. We then show that many important properties in separation logic, such as indivisible unit, disjointness, splittability, and cross-split, can be expressed in our general axiom form. Thus our framework offers inference rules and completeness for these properties for free. Finally, we show how our calculi reduce to calculi with global label substitutions, enabling more efficient implementation. △ Less

Submitted 26 March, 2018; v1 submitted 30 October, 2017; originally announced October 2017.

Comments: Accepted for publication in ACM Transactions on Computational Logic (TOCL). arXiv admin note: text overlap with arXiv:1307.5592

Formal Certification of Android Bytecode

Authors: Hendra Gunadi, Alwen Tiu, Rajeev Gore

Abstract: Android is an operating system that has been used in a majority of mobile devices. Each application in Android runs in an instance of the Dalvik virtual machine, which is a register-based virtual machine (VM). Most applications for Android are developed using Java, compiled to Java bytecode and then translated to DEX bytecode using the dx tool in the Android SDK. In this work, we aim to develop a… ▽ More Android is an operating system that has been used in a majority of mobile devices. Each application in Android runs in an instance of the Dalvik virtual machine, which is a register-based virtual machine (VM). Most applications for Android are developed using Java, compiled to Java bytecode and then translated to DEX bytecode using the dx tool in the Android SDK. In this work, we aim to develop a type-based method for certifying non-interference properties of DEX bytecode, following a methodology that has been developed for Java bytecode certification by Barthe et al. To this end, we develop a formal operational semantics of the Dalvik VM, a type system for DEX bytecode, and prove the soundness of the type system with respect to a notion of non-interference. We then study the translation process from Java bytecode to DEX bytecode, as implemented in the dx tool in the Android SDK. We show that an abstracted version of the translation from Java bytecode to DEX bytecode preserves the non-interference property. More precisely, we show that if the Java bytecode is typable in Barthe et al's type system (which guarantees non-interference) then its translation is typable in our type system. This result opens up the possibility to leverage existing bytecode verifiers for Java to certify non-interference properties of Android bytecode. △ Less

Submitted 6 October, 2016; v1 submitted 8 April, 2015; originally announced April 2015.

Comments: 12 pages content, 43 pages total including Appendices, double-column IEEE

Sequent Calculus in the Topos of Trees

Authors: Ranald Clouston, Rajeev Goré

Abstract: Nakano's "later" modality, inspired by Gödel-Löb provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show that the semantics of the propositional fragment of this logic can be given by linear converse-well-founded intuitionistic Kripke frames, so this logic is a m… ▽ More Nakano's "later" modality, inspired by Gödel-Löb provability logic, has been applied in type systems and program logics to capture guarded recursion. Birkedal et al modelled this modality via the internal logic of the topos of trees. We show that the semantics of the propositional fragment of this logic can be given by linear converse-well-founded intuitionistic Kripke frames, so this logic is a marriage of the intuitionistic modal logic KM and the intermediate logic LC. We therefore call this logic $\mathrm{KM}_{\mathrm{lin}}$. We give a sound and cut-free complete sequent calculus for $\mathrm{KM}_{\mathrm{lin}}$ via a strategy that decomposes implication into its static and irreflexive components. Our calculus provides deterministic and terminating backward proof-search, yields decidability of the logic and the coNP-completeness of its validity problem. Our calculus and decision procedure can be restricted to drop linearity and hence capture KM. △ Less

Submitted 17 April, 2015; v1 submitted 14 January, 2015; originally announced January 2015.

Comments: Extended version, with full proof details, of a paper accepted to FoSSaCS 2015 (this version edited to fix some minor typos)

Proof search for propositional abstract separation logics via labelled sequents

Authors: Zhe Hou, Ranald Clouston, Rajeev Gore, Alwen Tiu

Abstract: Separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called propositional abstract separation logics, extend the logic of (Boolean) Bunched Implications (BBI) in various ways. We develop a modular proof theory for var… ▽ More Separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called propositional abstract separation logics, extend the logic of (Boolean) Bunched Implications (BBI) in various ways. We develop a modular proof theory for various propositional abstract separation logics using cut-free labelled sequent calculi. We first extend the cut-fee labelled sequent calculus for BBI of Hou et al to handle Calcagno et al's original logic of separation algebras by adding sound rules for partial-determinism and cancellativity, while preserving cut-elimination. We prove the completeness of our calculus via a sound intermediate calculus that enables us to construct counter-models from the failure to find a proof. We then capture other propositional abstract separation logics by adding sound rules for indivisible unit and disjointness, while maintaining completeness. We present a theorem prover based on our labelled calculus for these propositional abstract separation logics. △ Less

Submitted 25 November, 2013; v1 submitted 22 July, 2013; originally announced July 2013.

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic -- Extended Version

Authors: Ranald Clouston, Jeremy Dawson, Rajeev Gore, Alwen Tiu

Abstract: Full Intuitionistic Linear Logic (FILL) is multiplicative intuitionistic linear logic extended with par. Its proof theory has been notoriously difficult to get right, and existing sequent calculi all involve inference rules with complex annotations to guarantee soundness and cut-elimination. We give a simple and annotation-free display calculus for FILL which satisfies Belnap's generic cut-elimina… ▽ More Full Intuitionistic Linear Logic (FILL) is multiplicative intuitionistic linear logic extended with par. Its proof theory has been notoriously difficult to get right, and existing sequent calculi all involve inference rules with complex annotations to guarantee soundness and cut-elimination. We give a simple and annotation-free display calculus for FILL which satisfies Belnap's generic cut-elimination theorem. To do so, our display calculus actually handles an extension of FILL, called Bi-Intuitionistic Linear Logic (BiILL), with an `exclusion' connective defined via an adjunction with par. We refine our display calculus for BiILL into a cut-free nested sequent calculus with deep inference in which the explicit structural rules of the display calculus become admissible. A separation property guarantees that proofs of FILL formulae in the deep inference calculus contain no trace of exclusion. Each such rule is sound for the semantics of FILL, thus our deep inference calculus and display calculus are conservative over FILL. The deep inference calculus also enjoys the subformula property and terminating backward proof search, which gives the NP-completeness of BiILL and FILL. △ Less

Submitted 18 July, 2013; v1 submitted 1 July, 2013; originally announced July 2013.

ACM Class: F.4.1

Epistemology of Modeling and Simulation: How can we gain Knowledge from Simulations?

Authors: Andreas Tolk, Saikou Y. Diallo, Jose J. Padilla, Ross Gore

Abstract: Epistemology is the branch of philosophy that deals with gaining knowledge. It is closely related to ontology. The branch that deals with questions like "What is real?" and "What do we know?" as it provides these components. When using modeling and simulation, we usually imply that we are doing so to either apply knowledge, in particular when we are using them for training and teaching, or that we… ▽ More Epistemology is the branch of philosophy that deals with gaining knowledge. It is closely related to ontology. The branch that deals with questions like "What is real?" and "What do we know?" as it provides these components. When using modeling and simulation, we usually imply that we are doing so to either apply knowledge, in particular when we are using them for training and teaching, or that we want to gain new knowledge, for example when doing analysis or conducting virtual experiments. This paper looks at the history of science to give a context to better cope with the question, how we can gain knowledge from simulation. It addresses aspects of computability and the general underlying mathematics, and applies the findings to validation and verification and development of federations. As simulations are understood as computable executable hypotheses, validation can be understood as hypothesis testing and theory building. The mathematical framework allows furthermore addressing some challenges when develo** federations and the potential introduction of contradictions when composing different theories, as they are represented by the federated simulation systems. △ Less

Submitted 21 June, 2013; originally announced June 2013.

Comments: MODSIM World 2013

MSC Class: 00

A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search

Authors: Zhe Hou, Alwen Tiu, Rajeev Gore

Abstract: We present a labelled sequent calculus for Boolean BI, a classical variant of O'Hearn and Pym's logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in our proof system, including those rules that manipulate labels, can be localised around applications of certain logical rules, thereby localising the handling of th… ▽ More We present a labelled sequent calculus for Boolean BI, a classical variant of O'Hearn and Pym's logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in our proof system, including those rules that manipulate labels, can be localised around applications of certain logical rules, thereby localising the handling of these rules in proof search. Based on this, we demonstrate a free variable calculus that deals with the structural rules lazily in a constraint system. A heuristic method to solve the constraints is proposed in the end, with some experimental results. △ Less

Submitted 3 May, 2015; v1 submitted 19 February, 2013; originally announced February 2013.

Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures

Authors: Alwen Tiu, Egor Ianovski, Rajeev Gore

Abstract: A grammar logic refers to an extension to the multi-modal logic K in which the modal axioms are generated from a formal grammar. We consider a proof theory, in nested sequent calculus, of grammar logics with converse, i.e., every modal operator [a] comes with a converse. Extending previous works on nested sequent systems for tense logics, we show all grammar logics (with or without converse) can b… ▽ More A grammar logic refers to an extension to the multi-modal logic K in which the modal axioms are generated from a formal grammar. We consider a proof theory, in nested sequent calculus, of grammar logics with converse, i.e., every modal operator [a] comes with a converse. Extending previous works on nested sequent systems for tense logics, we show all grammar logics (with or without converse) can be formalised in nested sequent calculi, where the axioms are internalised in the calculi as structural rules. Syntactic cut-elimination for these calculi is proved using a procedure similar to that for display logics. If the grammar is context-free, then one can get rid of all structural rules, in favor of deep inference and additional propagation rules. We give a novel semi-decision procedure for context-free grammar logics, using nested sequent calculus with deep inference, and show that, in the case where the given context-free grammar is regular, this procedure terminates. Unlike all other existing decision procedures for regular grammar logics in the literature, our procedure does not assume that a finite state automaton encoding the axioms is given. △ Less

Submitted 11 April, 2012; originally announced April 2012.

ACM Class: F.4.1

On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics

Authors: Rajeev Gore, Linda Postniece, Alwen F Tiu

Abstract: We consider two styles of proof calculi for a family of tense logics, presented in a formalism based on nested sequents. A nested sequent can be seen as a tree of traditional single-sided sequents. Our first style of calculi is what we call "shallow calculi", where inference rules are only applied at the root node in a nested sequent. Our shallow calculi are extensions of Kashima's calculus for t… ▽ More We consider two styles of proof calculi for a family of tense logics, presented in a formalism based on nested sequents. A nested sequent can be seen as a tree of traditional single-sided sequents. Our first style of calculi is what we call "shallow calculi", where inference rules are only applied at the root node in a nested sequent. Our shallow calculi are extensions of Kashima's calculus for tense logic and share an essential characteristic with display calculi, namely, the presence of structural rules called "display postulates". Shallow calculi enjoy a simple cut elimination procedure, but are unsuitable for proof search due to the presence of display postulates and other structural rules. The second style of calculi uses deep-inference, whereby inference rules can be applied at any node in a nested sequent. We show that, for a range of extensions of tense logic, the two styles of calculi are equivalent, and there is a natural proof theoretic correspondence between display postulates and deep inference. The deep inference calculi enjoy the subformula property and have no display postulates or other structural rules, making them a better framework for proof search. △ Less

Submitted 14 May, 2011; v1 submitted 28 March, 2011; originally announced March 2011.

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 7, Issue 2 (May 17, 2011) lmcs:971

Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic

Authors: Rajeev Gore, Linda Postniece, Alwen Tiu

Abstract: We consider an extension of bi-intuitionistic logic with the traditional modalities from tense logic Kt. Proof theoretically, this extension is obtained simply by extending an existing sequent calculus for bi-intuitionistic logic with typical inference rules for the modalities used in display logics. As it turns out, the resulting calculus, LBiKt, seems to be more basic than most intuitionistic te… ▽ More We consider an extension of bi-intuitionistic logic with the traditional modalities from tense logic Kt. Proof theoretically, this extension is obtained simply by extending an existing sequent calculus for bi-intuitionistic logic with typical inference rules for the modalities used in display logics. As it turns out, the resulting calculus, LBiKt, seems to be more basic than most intuitionistic tense or modal logics considered in the literature, in particular, those studied by Ewald and Simpson, as it does not assume any a priori relationship between the diamond and the box modal operators. We recover Ewald's intuitionistic tense logic and Simpson's intuitionistic modal logic by modularly extending LBiKt with additional structural rules. The calculus LBiKt is formulated in a variant of display calculus, using a form of sequents called nested sequents. Cut elimination is proved for LBiKt, using a technique similar to that used in display calculi. As in display calculi, the inference rules of LBiKt are ``shallow'' rules, in the sense that they act on top-level formulae in a nested sequent. The calculus LBiKt is ill-suited for backward proof search due to the presence of certain structural rules called ``display postulates'' and the contraction rules on arbitrary structures. We show that these structural rules can be made redundant in another calculus, DBiKt, which uses deep inference, allowing one to apply inference rules at an arbitrary depth in a nested sequent. We prove the equivalence between LBiKt and DBiKt and outline a proof search strategy for DBiKt. We also give a Kripke semantics and prove that LBiKt is sound with respect to the semantics, but completeness is still an open problem. We then discuss various extensions of LBiKt. △ Less

Submitted 28 June, 2010; v1 submitted 24 June, 2010; originally announced June 2010.

ACM Class: F.4.1

A Proof Theoretic Analysis of Intruder Theories

Authors: Alwen F Tiu, Rajeev Gore, Jeremy Dawson

Abstract: We consider the problem of intruder deduction in security protocol analysis: that is, deciding whether a given message M can be deduced from a set of messages Gamma under the theory of blind signatures and arbitrary convergent equational theories modulo associativity and commutativity (AC) of certain binary operators. The traditional formulations of intruder deduction are usually given in natural… ▽ More We consider the problem of intruder deduction in security protocol analysis: that is, deciding whether a given message M can be deduced from a set of messages Gamma under the theory of blind signatures and arbitrary convergent equational theories modulo associativity and commutativity (AC) of certain binary operators. The traditional formulations of intruder deduction are usually given in natural-deduction-like systems and proving decidability requires significant effort in showing that the rules are "local" in some sense. By using the well-known translation between natural deduction and sequent calculus, we recast the intruder deduction problem as proof search in sequent calculus, in which locality is immediate. Using standard proof theoretic methods, such as permutability of rules and cut elimination, we show that the intruder deduction problem can be reduced, in polynomial time, to the elementary deduction problem, which amounts to solving certain equations in the underlying individual equational theories. We show that this result extends to combinations of disjoint AC-convergent theories whereby the decidability of intruder deduction under the combined theory reduces to the decidability of elementary deduction in each constituent theory. To further demonstrate the utility of the sequent-based approach, we show that, for Dolev-Yao intruders, our sequent-based techniques can be used to solve the more difficult problem of solving deducibility constraints, where the sequents to be deduced may contain gaps (or variables) representing possible messages the intruder may produce. △ Less

Submitted 1 September, 2010; v1 submitted 25 May, 2010; originally announced May 2010.

Comments: Extended version of RTA 2009 paper

ACM Class: cs.CR

Journal ref: Logical Methods in Computer Science, Volume 6, Issue 3 (September 1, 2010) lmcs:877

Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse

Authors: Rajeev Goré, Florian Widmann

Abstract: We give an optimal (EXPTIME), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound methodto combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALC… ▽ More We give an optimal (EXPTIME), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound methodto combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL. △ Less

Submitted 15 April, 2010; v1 submitted 31 January, 2010; originally announced February 2010.

Comments: 30 pages, minor improvements, some typos, change of title

A decidable policy language for history-based transaction monitoring

Authors: Andreas Bauer, Rajeev Gore, Alwen Tiu

Abstract: Online trading invariably involves dealings between strangers, so it is important for one party to be able to judge objectively the trustworthiness of the other. In such a setting, the decision to trust a user may sensibly be based on that user's past behaviour. We introduce a specification language based on linear temporal logic for expressing a policy for categorising the behaviour patterns of… ▽ More Online trading invariably involves dealings between strangers, so it is important for one party to be able to judge objectively the trustworthiness of the other. In such a setting, the decision to trust a user may sensibly be based on that user's past behaviour. We introduce a specification language based on linear temporal logic for expressing a policy for categorising the behaviour patterns of a user depending on its transaction history. We also present an algorithm for checking whether the transaction history obeys the stated policy. To be useful in a real setting, such a language should allow one to express realistic policies which may involve parameter quantification and quantitative or statistical patterns. We introduce several extensions of linear temporal logic to cater for such needs: a restricted form of universal and existential quantification; arbitrary computable functions and relations in the term language; and a "counting" quantifier for counting how many times a formula holds in the past. We then show that model checking a transaction history against a policy, which we call the history-based transaction monitoring problem, is PSPACE-complete in the size of the policy formula and the length of the history. The problem becomes decidable in polynomial time when the policies are fixed. We also consider the problem of transaction monitoring in the case where not all the parameters of actions are observable. We formulate two such "partial observability" monitoring problems, and show their decidability under certain restrictions. △ Less

Submitted 17 March, 2009; originally announced March 2009.

A proof theoretic analysis of intruder theories

Authors: Alwen Tiu, Rajeev Gore

Abstract: We consider the problem of intruder deduction in security protocol analysis: that is, deciding whether a given message $M$ can be deduced from a set of messages $Γ$ under the theory of blind signatures and arbitrary convergent equational theories modulo associativity and commutativity (AC) of certain binary operators. The traditional formulations of intruder deduction are usually given in natura… ▽ More We consider the problem of intruder deduction in security protocol analysis: that is, deciding whether a given message $M$ can be deduced from a set of messages $Γ$ under the theory of blind signatures and arbitrary convergent equational theories modulo associativity and commutativity (AC) of certain binary operators. The traditional formulations of intruder deduction are usually given in natural-deduction-like systems and proving decidability requires significant effort in showing that the rules are "local" in some sense. By using the well-known translation between natural deduction and sequent calculus, we recast the intruder deduction problem as proof search in sequent calculus, in which locality is immediate. Using standard proof theoretic methods, such as permutability of rules and cut elimination, we show that the intruder deduction problem can be reduced, in polynomial time, to the elementary deduction problems, which amounts to solving certain equations in the underlying individual equational theories. We further show that this result extends to combinations of disjoint AC-convergent theories whereby the decidability of intruder deduction under the combined theory reduces to the decidability of elementary deduction in each constituent theory. Although various researchers have reported similar results for individual cases, our work shows that these results can be obtained using a systematic and uniform methodology based on the sequent calculus. △ Less

Submitted 6 April, 2009; v1 submitted 1 April, 2008; originally announced April 2008.

Comments: This is an extended version of a conference paper accepted to RTA 2009

ACM Class: F.3.1; F.4.1

An On-the-fly Tableau-based Decision Procedure for PDL-Satisfiability

Authors: Pietro Abate, Rajeev Goré, Florian Widmann

Abstract: We present a tableau-based algorithm for deciding satisfiability for propositional dynamic logic (PDL) which builds a finite rooted tree with ancestor loops and passes extra information from children to parents to separate good loops from bad loops during backtracking. It is easy to implement, with potential for parallelisation, because it constructs a pseudo-model ``on the fly'' by exploring ea… ▽ More We present a tableau-based algorithm for deciding satisfiability for propositional dynamic logic (PDL) which builds a finite rooted tree with ancestor loops and passes extra information from children to parents to separate good loops from bad loops during backtracking. It is easy to implement, with potential for parallelisation, because it constructs a pseudo-model ``on the fly'' by exploring each tableau branch independently. But its worst-case behaviour is 2EXPTIME rather than EXPTIME. A prototype implementation in the TWB (http://twb.rsise.anu.edu.au) is available. △ Less

Submitted 8 January, 2008; v1 submitted 7 November, 2007; originally announced November 2007.

Comments: 26 pages, longer version of article in Methods for Modalities 2007; improved readability of proofs

A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version

Authors: Linda Buisman, Rajeev Goré

Abstract: Bi-intuitionistic logic is the extension of intuitionistic logic with a connective dual to implication. Bi-intuitionistic logic was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ``cut-free'' sequent calculus for BiInt has recently been shown by Uustalu to fail cut-elimination. We present a new cut-free sequent calculus for BiInt, and prove it… ▽ More Bi-intuitionistic logic is the extension of intuitionistic logic with a connective dual to implication. Bi-intuitionistic logic was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ``cut-free'' sequent calculus for BiInt has recently been shown by Uustalu to fail cut-elimination. We present a new cut-free sequent calculus for BiInt, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between implication and its dual, similarly to future and past modalities in tense logic. Our calculus handles this interaction using extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of failed derivation trees. Our simple termination argument allows our calculus to be used for automated deduction, although this is not its main purpose. △ Less

Submitted 16 April, 2007; v1 submitted 13 April, 2007; originally announced April 2007.