Title :
A trace based extension of linear time temporal logic
Author :
Thiagarajan, P.S.
Author_Institution :
School of Math., SPIC Sci. Found., Madras, India
Abstract :
The propositional temporal logic of linear time (PTL) is interpreted over linear orders of order type (ω,⩽). In applications, these linear orders consist of interleaved descriptions of the infinite runs of a concurrent program. Recent research on partial order based verification methods suggests that it might be fruitful to represent such runs as partial orders called infinite traces. We design a natural extension of PTL called TrPTL to be interpreted directly over infinite traces. Using automata-theoretic techniques we show that the satisfiability problem for TrPTL is decidable. The automata that arise in this context turn out to be an attractive model of finite state concurrent programs. As a result, we also solve the model checking problem for TrPTL with respect to finite state concurrent programs
Keywords :
decidability; finite automata; multiprocessing programs; programming theory; temporal logic; TrPTL; automata theory; concurrent program; decidability; finite state concurrent programs; infinite runs; infinite traces; interleaved descriptions; linear orders; linear time temporal logic; model checking problem; partial order based verification methods; propositional temporal logic; satisfiability problem; trace based extension; Automata; Concurrent computing; Context modeling; Labeling; Logic; Mathematics;
Conference_Titel :
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location :
Paris
Print_ISBN :
0-8186-6310-3
DOI :
10.1109/LICS.1994.316047