A trace based extension of linear time temporal logic

Abstract

The propositional temporal logic of linear time (PTL) is interpreted over linear orders of order type (/spl omega/,/spl les/). 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.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>