Complexity of propositional projection temporal logic with star

2009 ◽  
Vol 19 (1) ◽  
pp. 73-100 ◽  
Author(s):  
CONG TIAN ◽  
ZHENHUA DUAN
Keyword(s):  
Lower Bound ◽  
Normal Form ◽  
Temporal Logic ◽  
Decision Algorithm ◽  
Emptiness Problem ◽  
Form Graph

This paper investigates the complexity of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Propositional Projection Temporal Logic (PPTL) is first extended to include projection star. Then, by reducing the emptiness problem of star-free expressions to the problem of the satisfiability of PPTL* formulas, the lower bound of the complexity for the satisfiability of PPTL* formulas is proved to be non-elementary. Then, to prove the decidability of PPTL*, the normal form, normal form graph (NFG) and labelled normal form graph (LNFG) for PPTL* are defined. Also, algorithms for transforming a formula to its normal form and LNFG are presented. Finally, a decision algorithm for checking the satisfiability of PPTL* formulas is formalised using LNFGs.

Algorithm for Decision Procedure in Temporal Logic Treating Uncertainty, Plausibility, Knowledge and Interacting Agents

2012 ◽  
pp. 32-46
Author(s):  
V. Rybakov
Keyword(s):  
Normal Form ◽  
Temporal Logic ◽  
Decision Procedure ◽  
Linear Temporal Logic ◽  
Satisfiability Problem ◽  
Global Knowledge ◽  
Interacting Agents ◽  
Logical Operations ◽  
Multi Agent ◽  
Bounded Size

Our paper studies a logic UIALTL, which is a combination of the linear temporal logic LTL, a multi-agent logic with operation for passing knowledge via agents’ interaction, and a suggested logic based on operation of logical uncertainty. The logical operations of UIALTL also include (together with operations from LTL) operations of strong and weak until, agents’ knowledge operations, operation of knowledge via interaction, operation of logical uncertainty, the operations for environmental and global knowledge. UIALTL is defined as a set of all formulas valid at all Kripke-Hintikka like models NC. Any frame NC represents possible unbounded (in time) computation with multi-processors (parallel computational units) and agents’ channels for connections between computational units. The main aim of our paper is to determine possible ways for computation logical laws of UIALTL. Principal problems we are dealing with are decidability and the satisfiability problems for UIALTL. We find an algorithm which recognizes theorems of UIALTL (so we show that UIALTL is decidable) and solves satisfiability problem for UIALTL. As an instrument we use reduction of formulas to rules in the reduced normal form and a technique to contract models NC to special non-UIALTL-models, and, then, verification of validity these rules in models of bounded size. The paper uses standard results from non-classical logics based on Kripke-Hintikka models.

Towards a Normal Form and a Query Language for Extended Relations Defined by Regular Expressions

2016 ◽  
Vol 27 (2) ◽  
pp. 27-48
Author(s):  
András Benczúr ◽  
Gyula I. Szabó
Keyword(s):  
Normal Form ◽  
Data Base ◽  
Data Model ◽  
Query Language ◽  
Xml Schema ◽  
Relational Model ◽  
Regular Expressions ◽  
Functional Dependencies ◽  
Decision Algorithm ◽  
Implication Problem

This paper introduces a generalized data base concept that unites relational and semi structured data models. As an important theoretical result we could find a quadratic decision algorithm for the implication problem of functional and join dependencies defined on the united data model. As practical contribution we presented a normal form for the new data model as a tool for data base design. With our novel representations of regular expressions, a more effective searching method could be developed. XML elements are described by XML schema languages such as a DTD or an XML Schema definition. The instances of these elements are semi-structured tuples. A semi-structured tuple is an ordered list of (attribute: value) pairs. We may think of a semi-structured tuple as a sentence of a formal language, where the values are the terminal symbols and the attribute names are the non-terminal symbols. In the authors' former work (Szabó and Benczúr, 2015) they introduced the notion of the extended tuple as a sentence from a regular language generated by a grammar where the non-terminal symbols of the grammar are the attribute names of the tuple. Sets of extended tuples are the extended relations. The authors then introduced the dual language, which generates the tuple types allowed to occur in extended relations. They defined functional dependencies (regular FD - RFD) over extended relations. In this paper they rephrase the RFD concept by directly using regular expressions over attribute names to define extended tuples. By the help of a special vertex labeled graph associated to regular expressions the specification of substring selection for the projection operation can be defined. The normalization for regular schemas is more complex than it is in the relational model, because the schema of an extended relation can contain an infinite number of tuple types. However, the authors can define selection, projection and join operations on extended relations too, so a lossless-join decomposition can be performed. They extended their previous model to deal with XML schema indicators too, e.g., with numerical constraints. They added line and set constructors too, in order to extend their model with more general projection and selection operators. This model establishes a query language with table join functionality for collected XML element data.

Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete

2017 ◽  
Vol 28 (08) ◽  
pp. 945-975 ◽  
Author(s):  
Mohamed Faouzi Atig ◽  
Benedikt Bollig ◽  
Peter Habermehl
Keyword(s):  
Lower Bound ◽  
Turing Machine ◽  
Linear Ordering ◽  
Emptiness Problem ◽  
Pushdown Automata ◽  
Exponential Space

We consider ordered multi-pushdown automata, a multi-stack extension of pushdown automata that comes with a constraint on stack operations: a pop can only be performed on the first non-empty stack (which implies that we assume a linear ordering on the collection of stacks). We show that the emptiness problem for multi-pushdown automata is 2ETIME-complete. Containment in 2ETIME is shown by translating an automaton into a grammar for which we can check if the generated language is empty. The lower bound is established by simulating the behavior of an alternating Turing machine working in exponential space. We also compare ordered multi-pushdown automata with the model of bounded-phase (visibly) multi-stack pushdown automata, which do not impose an ordering on stacks, but restrict the number of alternations of pop operations on different stacks.

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.

Poincaré Maps of “ <”-Shape Planar Piecewise Linear Dynamical Systems with a Saddle

2019 ◽  
Vol 29 (12) ◽  
pp. 1950165
Author(s):  
Qianqian Zhao ◽  
Jiang Yu
Keyword(s):  
Dynamical Systems ◽  
Lower Bound ◽  
Normal Form ◽  
Limit Cycle ◽  
Limit Cycles ◽  
Inflection Point ◽  
Piecewise Linear ◽  
Poincaré Maps ◽  
Linear Dynamical Systems ◽  
Poincare Maps

It is important in the study of limit cycles to investigate the properties of Poincaré maps of discontinuous dynamical systems. In this paper, we focus on a class of planar piecewise linear dynamical systems with “[Formula: see text]”-shape regions and prove that the Poincaré map of a subsystem with a saddle has at most one inflection point which can be reached. Furthermore, we show that one class of such systems with a saddle-center has at least three limit cycles; a class of such systems with saddle and center in the normal form has at most one limit cycle which can be reached; and a class of such systems with saddle and center at the origin has at most three limit cycles with a lower bound of two. We try to reveal the reasons for the increase of the number of limit cycles when the discontinuity happens to a system.

Algorithm for Decision Procedure in Temporal Logic Treating Uncertainty, Plausibility, Knowledge and Interacting Agents

2010 ◽  
Vol 6 (1) ◽  
pp. 31-45 ◽  
Author(s):  
V. Rybakov
Keyword(s):  
Normal Form ◽  
Temporal Logic ◽  
Decision Procedure ◽  
Linear Temporal Logic ◽  
Satisfiability Problem ◽  
Global Knowledge ◽  
Interacting Agents ◽  
Logical Operations ◽  
Multi Agent ◽  
Bounded Size

Our article studies logic UIALTL, which is a combination of the linear temporal logic LTL, a multi-agent logic with operation for passing knowledge via agents’ interaction, and a suggested logic based on operation of logical uncertainty. The logical operations of UIALTL also include (together with operations from LTL) operations of strong and weak until, agents’ knowledge operations, operation of knowledge via interaction, operation of logical uncertainty, the operations for environmental and global knowledge. UIALTL is defined as a set of all formulas valid at all Kripke-Hintikka like models NC. Any frame NC represents possible unbounded (in time) computation with multi-processors (parallel computational units) and agents’ channels for connections between computational units. The main aim of our article is to determine possible ways for computation logical laws of UIALTL. Principal problems we are dealing with are decidability and the satisfiability problems for UIALTL. We find an algorithm which recognizes theorems of UIALTL (so we show that UIALTL is decidable) and solves satisfiability problem for UIALTL. As an instrument we use reduction of formulas to rules in the reduced normal form and a technique to contract models NC to special non-UIALTL-models, and, then, verification of validity these rules in models of bounded size. The article uses standard results from non-classical logics based on Kripke-Hintikka models.

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