scholarly journals Temporal Logics Beyond Regularity

2007 ◽  
Vol 14 (13) ◽  
Author(s):  
Martin Lange
Keyword(s):  
Model Checking ◽  
Dynamic Logic ◽  
Expressive Power ◽  
Turing Machines ◽  
Temporal Logics ◽  
Propositional Dynamic Logic ◽  
Program Correctness ◽  
Recursive Procedures ◽  
Language Classes ◽  
Context Free

Non-regular program correctness properties play an important role in the specification of unbounded buffers, recursive procedures, etc. This thesis surveys results about the relative expressive power and complexity of temporal logics which are capable of defining non-regular properties. In particular, it features Propositional Dynamic Logic of Context-Free Programs, Fixpoint Logic with Chop, the Modal Iteration Calculus, and Higher-Order Fixpoint Logic.<br /> <br />Regarding expressive power we consider two classes of structures: arbitrary transition systems as well as finite words as a subclass of the former. The latter is meant to give an intuitive account of the logics' expressive powers by relating them to known language classes defined in terms of grammars or Turing Machines. <br /> <br /> Regarding the computational complexity of temporal logics beyond regularity we focus on their model checking problems since their satisfiability problems are all highly undecidable. Their model checking complexities range between polynomial time and non-elementary.

Propositional dynamic logic of context-free programs

1981 ◽  
Author(s):  
David Harel ◽  
Amir Pnueli ◽  
Jonathan Stavi
Keyword(s):  
Dynamic Logic ◽  
Propositional Dynamic Logic ◽  
Context Free

scholarly journals On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

2021 ◽  
Vol 28 (4) ◽  
pp. 356-371
Author(s):  
Anton Romanovich Gnatenko ◽  
Vladimir Anatolyevich Zakharov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Time ◽  
Complete Solution ◽  
Reactive Systems ◽  
Expressive Power ◽  
Regular Languages ◽  
Specification Languages ◽  
Temporal Logics ◽  
Emptiness Problem

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

scholarly journals Complexity Results for Model Checking

1995 ◽  
Vol 2 (18) ◽  
Author(s):  
Allan Cheng
Keyword(s):  
Model Checking ◽  
Linear Time ◽  
Kripke Model ◽  
Upper Bounds ◽  
Polynomial Space ◽  
Turing Machines ◽  
Temporal Logics ◽  
Kripke Structures ◽  
Np Complete ◽  
Exponential Space

The complexity of model checking branching and linear time<br />temporal logics over Kripke structures has been addressed in e.g. [SC85,<br />CES86]. In terms of the size of the Kripke model and the length of the<br />formula, they show that the model checking problem is solvable in <br />polynomial time for CTL and NP-complete for L(F). The model checking<br />problem can be generalised by allowing more succinct descriptions of<br />systems than Kripke structures. We investigate the complexity of the<br />model checking problem when the instances of the problem consist of<br />a formula and a description of a system whose state space is at most<br />exponentially larger than the description. Based on Turing machines,<br />we define compact systems as a general formalisation of such system<br />descriptions. Examples of such compact systems are K-bounded Petri<br />nets and synchronised automata, and in these cases the well-known <br />algorithms presented in [SC85, CES86] would require exponential space in<br />term of the sizes of the system descriptions and the formulas; we present<br />polynomial space upper bounds for the model checking problem over<br />compact systems and the logics CTL and L(X,U,S). As an example of<br />an application of our general results we show that the model checking<br />problems of both the branching time temporal logic CTL and the linear<br />time temporal logics L(F) and L(X,U, S) over K-bounded Petri nets are<br />PSPACE-complete.

scholarly journals Model-Checking Structured Context-Free Languages

2021 ◽  
pp. 387-410
Author(s):  
Michele Chiari ◽  
Dino Mandrioli ◽  
Matteo Pradella
Keyword(s):  
Model Checking ◽  
Use Cases ◽  
Temporal Logics ◽  
Local Properties ◽  
Nested Words ◽  
Checking Procedure ◽  
Definition Of ◽  
And Function ◽  
Context Free

AbstractThe problem of model checking procedural programs has fostered much research towards the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and NWTL. Recently, the logic OPTL was introduced, based on the class of Operator Precedence Languages (OPL), more powerful than Nested Words. We define the new OPL-based logic POTL, and provide a model checking procedure for it. POTL improves on NWTL by enabling the formulation of requirements involving pre/post-conditions, stack inspection, and others in the presence of exception-like constructs. It improves on OPTL by being FO-complete, and by expressing more easily stack inspection and function-local properties. We developed a model checking tool for POTL, which we experimentally evaluate on some interesting use-cases.

The Influence of the Test Operator on the Expressive Power of PDL-like Logics

2019 ◽  
Vol 29 (8) ◽  
pp. 1289-1310
Author(s):  
Linh Anh Nguyen
Keyword(s):  
Description Logics ◽  
Dynamic Logic ◽  
Expressive Power ◽  
Propositional Dynamic Logic ◽  
Test Operator ◽  
Local Reflexivity ◽  
Horn Fragment ◽  
Logical Formalism

Abstract Berman and Paterson proved that test-free propositional dynamic logic (PDL) is weaker than PDL. One would raise questions: does a similar result also hold for extensions of PDL? For example, is test-free converse-PDL (CPDL) weaker than CPDL? In what circumstances the test operator can be eliminated without reducing the expressive power of a PDL-based logical formalism? These problems have not yet been studied. As the description logics $\mathcal{ALC}_{trans}$ and $\mathcal{ALC}_{reg}$ are, respectively, variants of test-free PDL and PDL, there is a concept of $\mathcal{ALC}_{reg}$ that is not equivalent to any concept of $\mathcal{ALC}_{trans}$. Generalizing this, we prove that there is a concept of $\mathcal{ALC}_{reg}$ that is not equivalent to any concept of the logic that extends $\mathcal{ALC}_{trans}$ with inverse roles, nominals, qualified number restrictions, the universal role and local reflexivity of roles. We also provide some results for the case with RBoxes and TBoxes. One of them states that tests can be eliminated from TBoxes of the deterministic Horn fragment of $\mathcal{ALC}_{reg}$.

scholarly journals On the Model Checking Problem for Some Extension of CTL*

2020 ◽  
Vol 27 (4) ◽  
pp. 428-441
Author(s):  
Anton Romanovich Gnatenko ◽  
Vladimir Anatolyevich Zakharov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Reactive Systems ◽  
Expressive Power ◽  
Binary Relations ◽  
Temporal Logics ◽  
Distinctive Features ◽  
Verification Problem ◽  
Finite State ◽  
Infinite Sequences

Sequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The result of the operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often used as formal models for them. The behavior of transducers is represented by binary relations on infinite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL, mu-calculus) are poorly suited as specification languages, since omega-languages, not binary relations on omega-words are used for interpretation of their formulae. To provide temporal logics with the ability to define properties of transformations that characterize the behavior ofreactive systems, we introduced new extensions ofthese logics, which have two distinctive features: 1) temporal operators are parameterized, and languages in the input alphabet oftransducers are used as parameters; 2) languages in the output alphabet oftransducers are used as basic predicates. Previously, we studied the expressive power ofnew extensions Reg-LTL and Reg-CTL ofthe well-known temporal logics oflinear and branching time LTL and CTL, in which it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. We discovered that such a parameterization increases the expressive capabilities oftemporal logic, but preserves the decidability of the model checking problem. For the logics mentioned above, we have developed algorithms for the verification of finite transducers. At the next stage of our research on the new extensions of temporal logic designed for the specification and verification of sequential reactive systems, we studied the verification problem for these systems using the temporal logic Reg-CTL*, which is an extension ofthe Generalized Computational Tree Logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulae on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace.

PDL with intersection and converse: satisfiability and infinite-state model checking

2009 ◽  
Vol 74 (1) ◽  
pp. 279-314 ◽  
Author(s):  
Stefan Göller ◽  
Markus Lohrey ◽  
Carsten Lutz
Keyword(s):  
Lower Bound ◽  
Model Checking ◽  
Dynamic Logic ◽  
State Model ◽  
Propositional Dynamic Logic ◽  
Reasoning Problem ◽  
Infinite Trees ◽  
Emptiness Problem ◽  
Alternating Turing Machines ◽  
Infinite State

AbstractWe study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2ΕΧΡΤΙΜΕ, thus 2ΕΧΡΤΙΜΕ-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2ΕΧΡΤΙΜΕ-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2ΕΧΡΤΙΜΕ. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines.

Sign in / Sign up

Export Citation Format

Share Document