Paper Info
Title
On The Satisfiability Problem For Lamport'S Propositional Temporal Logic Of Actions And Some Of Its Extensions
Abstract
The Temporal Logic of Actions (TLA) devised by Lamport is a logic for proving the correctness of concurrent systems. A distinctive feature of the logic is the use of “action formulae” to encode the “before-after” behaviour of transitions, a feature that is especially suitable for Lamport's transition-axiom method. Abadi has given a complete axiomatization for the propositional fragment of this logic, and conjectured that its validity problem may be in PSPACE. In this paper we confirm that conjecture. In fact we show that the validity problem for TLA is PSPACE-complete. For this we give a space-optimal automata-theoretic decision procedure for TLA. Our result is obtained with respect to a logic which is a conservative extension of Lamport's TLA. Thus our decision procedure applies to the more restricted logic. We show how the automata-theoretic framework handles abstraction, as used in TLA, a feature considered useful for hierarchical and compositional reasoning.
Year
DOI
Venue
1995
10.3233/FI-1995-2444
Fundam. Inform.
Keywords
Field
DocType
automata-theoretic framework,distinctive feature,decision procedure,temporal logic,action formula,validity problem,compositional reasoning,complete axiomatization,space-optimal automata-theoretic decision procedure,propositional temporal logic,restricted logic,satisfiability problem,satisfiability,temporal logic of actions
Discrete mathematics,Modal μ-calculus,Autoepistemic logic,Temporal logic of actions,Interval temporal logic,Zeroth-order logic,Linear temporal logic,Intermediate logic,Mathematics,Dynamic logic (modal logic)
Journal
Volume
Issue
Citations 
24
4
0
PageRank 
References 
Authors
0.34
10
1
Name
Order
Citations
PageRank
Y.S. Ramakrishna1101.66