Logic in Computer Science (LICS 1994)

Paper: A trace based extension of linear time temporal logic (at LICS 1994)

Authors: P. S. Thiagarajan

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

BibTeX

  @InProceedings{Thiagarajan-Atracebasedextensio,
    author = 	 {P. S. Thiagarajan},
    title = 	 {A trace based extension of linear time temporal logic},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994},
    year =	 1994,
    editor =	 {Samson Abramsky},
    month =	 {July}, 
    pages =      {438--447},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }