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 REASONING ABOUT TRANSFINITE SEQUENCES

2007 ◽  
Vol 18 (01) ◽  
pp. 87-112 ◽  
Author(s):  
STÉPHANE DEMRI ◽  
DAVID NOWAK
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Time ◽  
Temporal Logics ◽  
Future Time ◽  
New Class ◽  
Linear Time Temporal Logic ◽  
Do So ◽  
Time Operators

We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on ω-sequences but interact synchronously with the system in order to restrict their behaviors. We show that the satisfiability and model-checking for the logics working on ωk-sequences is EXPSPACE-complete when the integers are represented in binary, and PSPACE-complete with a unary representation. To do so, we substantially extend standard results about LTL by introducing a new class of succinct ordinal automata that can encode the interaction between the different quantitative temporal operators.

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 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.

scholarly journals Fractal Dimension versus Process Complexity

2016 ◽  
Vol 2016 ◽  
pp. 1-21 ◽  
Author(s):  
Joost J. Joosten ◽  
Fernando Soler-Toscano ◽  
Hector Zenil
Keyword(s):  
Fractal Dimension ◽  
Turing Machine ◽  
Time Complexity ◽  
Linear Time ◽  
Space Time ◽  
Polynomial Space ◽  
Turing Machines ◽  
Complexity Measures ◽  
Strong Relation ◽  
Process Complexity

We look at small Turing machines (TMs) that work with just two colors (alphabet symbols) and either two or three states. For any particular such machineτand any particular inputx, we consider what we call thespace-timediagram which is basically the collection of consecutive tape configurations of the computationτ(x). In our setting, it makes sense to define a fractal dimension for a Turing machine as the limiting fractal dimension for the corresponding space-time diagrams. It turns out that there is a very strong relation between the fractal dimension of a Turing machine of the above-specified type and its runtime complexity. In particular, a TM with three states and two colors runs in at most linear time, if and only if its dimension is 2, and its dimension is 1, if and only if it runs in superpolynomial time and it uses polynomial space. If a TM runs in timeO(xn), we have empirically verified that the corresponding dimension is(n+1)/n, a result that we can only partially prove. We find the results presented here remarkable because they relate two completely different complexity measures: the geometrical fractal dimension on one side versus the time complexity of a computation on the other side.

scholarly journals Total Roman {3}-Domination: The Complexity and Linear-Time Algorithm for Trees

Mathematics ◽  
2021 ◽  
Vol 9 (3) ◽  
pp. 293
Author(s):  
Xinyue Liu ◽  
Huiqin Jiang ◽  
Pu Wu ◽  
Zehui Shao
Keyword(s):  
Linear Time ◽  
Minimum Weight ◽  
Domination Number ◽  
Time Algorithm ◽  
Simple Graph ◽  
Linear Time Algorithm ◽  
Domination Problem ◽  
Np Complete ◽  
Chordal Bipartite Graphs ◽  
Dominating Function

For a simple graph G=(V,E) with no isolated vertices, a total Roman {3}-dominating function(TR3DF) on G is a function f:V(G)→{0,1,2,3} having the property that (i) ∑w∈N(v)f(w)≥3 if f(v)=0; (ii) ∑w∈N(v)f(w)≥2 if f(v)=1; and (iii) every vertex v with f(v)≠0 has a neighbor u with f(u)≠0 for every vertex v∈V(G). The weight of a TR3DF f is the sum f(V)=∑v∈V(G)f(v) and the minimum weight of a total Roman {3}-dominating function on G is called the total Roman {3}-domination number denoted by γt{R3}(G). In this paper, we show that the total Roman {3}-domination problem is NP-complete for planar graphs and chordal bipartite graphs. Finally, we present a linear-time algorithm to compute the value of γt{R3} for trees.

scholarly journals An Efficient Simulation of Polynomial-Space Turing Machines by P Systems with Active Membranes

2010 ◽  
pp. 461-478 ◽  
Author(s):  
Andrea Valsecchi ◽  
Antonio E. Porreca ◽  
Alberto Leporati ◽  
Giancarlo Mauri ◽  
Claudio Zandron
Keyword(s):  
P Systems ◽  
Polynomial Space ◽  
Turing Machines ◽  
Efficient Simulation ◽  
Active Membranes

scholarly journals Model Checking Temporal Epistemic Logic under Bounded Recall

2020 ◽  
Vol 34 (05) ◽  
pp. 7071-7078
Author(s):  
Francesco Belardinelli ◽  
Alessio Lomuscio ◽  
Emily Yu
Keyword(s):  
Model Checking ◽  
Incomplete Information ◽  
Epistemic Logic ◽  
Upper Bounds ◽  
Experimental Results ◽  
Model Checker ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Multi Agent ◽  
Bounded Recall

We study the problem of verifying multi-agent systems under the assumption of bounded recall. We introduce the logic CTLKBR, a bounded-recall variant of the temporal-epistemic logic CTLK. We define and study the model checking problem against CTLK specifications under incomplete information and bounded recall and present complexity upper bounds. We present an extension of the BDD-based model checker MCMAS implementing model checking under bounded recall semantics and discuss the experimental results obtained.

Sign in / Sign up

Export Citation Format

Share Document