Undecidability of QLTL with two variables and one monadic predicate letter

We study the algorithmic properties of the quantified linear-time temporal logic QLTL in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We prove that the satisfiability problem for QLTL in languages with two individual variables and one monadic predicate letter in Σ 11 -hard. Thus, QLTL is Π 11 -hard, and so not recursively enumerable, in such languages. The resultholds both for the increasing domain and the constant domain semantics and is obtained by reduction from a Σ 11 -hard N×N recurrent tiling problem. It follows from the proof for QLTL that similar results hold for the quantified branching-time temporal logic QCTL, and hence for the quantified alternating-time temporal logic QATL. The result presented in this paper strengthens a result by I. Hodkinson, F. Wolter, and M. Zakharyaschev, who have shown that the satisfiability problem for QLTL is Σ 11 -hard in languages with two individual variablesand an unlimited supply of monadic predicate letters.

Download Full-text

AN NP-COMPLETE FRAGMENT OF LTL

International Journal of Foundations of Computer Science ◽

10.1142/s0129054105003261 ◽

2005 ◽

Vol 16 (04) ◽

pp. 743-753 ◽

Cited By ~ 6

Author(s):

ANCA MUSCHOLL ◽

IGOR WALUKIEWICZ

Keyword(s):

Temporal Logic ◽

Linear Time ◽

Satisfiability Problem ◽

Linear Time Temporal Logic ◽

Np Complete

A fragment of linear time temporal logic (LTL) is presented. It is proved that the satisfiability problem for this fragment is NP-complete. The fragment is larger than previously known NP-complete fragments. It is obtained by prohibiting the use of until operator and requiring to use only next operators indexed by a letter.

Download Full-text

Verifying linear time temporal logic properties of concurrent Ada programs with quasar

ACM SIGAda Ada Letters ◽

10.1145/992211.958424 ◽

2004 ◽

Vol XXIV (1) ◽

pp. 17-24 ◽

Cited By ~ 3

Author(s):

S. Evangelista ◽

C. Kaiser ◽

J. F. Pradat-Peyre ◽

P. Rousseau

Keyword(s):

Temporal Logic ◽

Linear Time ◽

Linear Time Temporal Logic

Download Full-text

Vehicle route-sequence planning using temporal logic

Artificial intelligence for engineering design analysis and manufacturing ◽

10.1017/s0890060401020042 ◽

2002 ◽

Vol 16 (1) ◽

pp. 31-38

Author(s):

KIAM TIAN SEOW ◽

MICHEL PASQUIER

Keyword(s):

Temporal Logic ◽

Linear Time ◽

Simple Procedure ◽

Precedence Constraints ◽

Sequence Planning ◽

Vehicle Route ◽

Passenger Travel ◽

State Formula ◽

Linear Time Temporal Logic ◽

Service Task

This paper proposes a new logical framework for vehicle route-sequence planning of passenger travel requests. Each request is a fetch-and-send service task associated with two request-locations, namely, a source and a destination. The proposed framework is developed using propositional linear time temporal logic of Manna and Pnueli. The novelty lies in the use of the formal language for both the specification and theorem-proving analysis of precedence constraints among the location visits that are inherent in route sequences. In the framework, legal route sequences—each of which visits every request location once and only once in the precedence order of fetch-and-send associated with every such request—is formalized and justified, forming a basis upon which the link between a basic precedence constraint and the corresponding canonical forbidden-state formula is formally established. Over a given base route plan, a simple procedure to generate a feasible subplan based on a specification of the forbidden-state canonical form is also given. An example demonstrates how temporal logic analysis and the proposed procedure can be applied to select a final (feasible) subplan based on additional precedence constraints.

Download Full-text

On-the-fly automata construction for dynamic linear time temporal logic

Proceedings. 11th International Symposium on Temporal Representation and Reasoning, 2004. TIME 2004. ◽

10.1109/time.2004.1314430 ◽

2004 ◽

Cited By ~ 3

Author(s):

L. Giordano ◽

A. Martelli

Keyword(s):

Temporal Logic ◽

Linear Time ◽

Linear Time Temporal Logic

Download Full-text

Ein Ansatz zur formalen Verifikation von Schaltungsbeschreibungen in SystemC (An Approach for Formal Verification of Circuits in SystemC)

it - Information Technology ◽

10.1524/itit.45.4.219.22731 ◽

2003 ◽

Vol 45 (4) ◽

Cited By ~ 1

Author(s):

Daniel Große ◽

Rolf Drechsler

Keyword(s):

Formal Verification ◽

Temporal Logic ◽

Linear Time ◽

Linear Time Temporal Logic

ZusammenfassungDer vorgestellte Ansatz ermöglicht es, für SystemC-Schaltkreisbeschreibungen, die über einer gegebenen Gatterbibliothek definiert sind, Eigenschaften zu beweisen (engl. property checking). Als Spezifikationssprache wird LTL (linear time temporal logic) verwendet. Für den Beweis einer LTL-Eigenschaft kann die Erfüllbarkeit einer Booleschen Funktion betrachtet werden, die aus der Eigenschaft und der Schaltkreisbeschreibung mittels symbolischer Methoden konstruiert wird. Im Gegensatz zu simulationsbasierten Ansätzen kann dabei Vollständigkeit gewährleistet werden. Anhand einer Fallstudie eines skalierbaren Arbiters wird die Effizienz des Beweisverfahrens untersucht.

Download Full-text

Verifying Fault-Tolerance in Probabilistic Swarm Systems

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2020/46 ◽

2020 ◽

Author(s):

Alessio Lomuscio ◽

Edoardo Pirovano

Keyword(s):

Fault Tolerance ◽

Temporal Logic ◽

Decision Problem ◽

Swarm Robotics ◽

Linear Time ◽

Experimental Results ◽

Robotic Swarms ◽

Linear Time Temporal Logic ◽

Probabilistic Nature

We present a method for reasoning about fault-tolerance in unbounded robotic swarms. We introduce a novel semantics that accounts for the probabilistic nature of both the swarm and possible malfunctions, as well as the unbounded nature of swarm systems. We define and interpret a variant of probabilistic linear-time temporal logic on the resulting executions, including those arising from faulty behaviour by some of the agents in the swarm. We specify the decision problem of parameterised fault-tolerance, which concerns determining whether a probabilistic specification holds under possibly faulty behaviour. We outline a verification procedure that we implement and use to study a foraging protocol from swarm robotics, and report the experimental results obtained.

Download Full-text

Combining linear-time temporal logic with constructiveness and paraconsistency

Journal of Applied Logic ◽

10.1016/j.jal.2009.06.001 ◽

2010 ◽

Vol 8 (1) ◽

pp. 33-61 ◽

Cited By ~ 22

Author(s):

Norihiro Kamide ◽

Heinrich Wansing

Keyword(s):

Temporal Logic ◽

Linear Time ◽

Linear Time Temporal Logic

Download Full-text

Dynamic Linear Time Temporal Logic

BRICS Report Series ◽

10.7146/brics.v4i8.18798 ◽

1997 ◽

Vol 4 (8) ◽

Cited By ~ 2

Author(s):

Jesper G. Henriksen ◽

P. S. Thiagarajan

Keyword(s):

Temporal Logic ◽

Linear Time ◽

Dynamic Logic ◽

Order Theory ◽

Simple Extension ◽

Propositional Dynamic Logic ◽

First Order ◽

Time Semantics ◽

Linear Time Temporal Logic ◽

Obvious Manner

A simple extension of the propositional temporal logic of linear time is proposed. The extension consists of strengthening the until operator by indexing it with the regular programs of propositional dynamic logic (PDL). It is shown that DLTL, the resulting logic, is expressively equivalent to S1S, the monadic second-order theory of omega-sequences. In fact a sublogic of DLTL which corresponds to propositional dynamic logic with a linear time semantics is already as expressive as S1S. We pin down in an obvious manner the sublogic of DLTL which correponds to the first order fragment of S1S. We show that DLTL has an exponential time decision procedure. We also obtain an axiomatization of DLTL. Finally, we point to some natural extensions of the approach presented here for bringing together propositional dynamic and temporal logics in a linear time setting.

Download Full-text