DocumentCode :
1995821
Title :
A trace based extension of linear time temporal logic
Author :
Thiagarajan, P.S.
Author_Institution :
School of Math., SPIC Sci. Found., Madras, India
fYear :
1994
fDate :
4-7 Jul 1994
Firstpage :
438
Lastpage :
447
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
Conference_Location :
Paris
Print_ISBN :
0-8186-6310-3
Type :
conf
DOI :
10.1109/LICS.1994.316047
Filename :
316047
Link To Document :
بازگشت