publication . Conference object . 2007

bi-infinite time in the verification of temporal properties

Matteo Pradella; Angelo Morzenti; Pierluigi San Pietro;
  • Published: 26 Sep 2007
  • Publisher: ACM Press
Model checking techniques have traditionally dealt with temporal logic languages and automata interpreted over ω-words, i.e., infinite in the future but finite in the past. However, time with also an infinite past is a useful abstraction in specification. It allows one to ignore the complexity of system initialization in much the same way as system termination may be abstracted away by allowing an infinite future. One can then write specifications that are simpler and more easily understandable, because they do not include the description of the operations (such as configuration or installation) typically performed at system deployment time. The present paper is...
free text keywords: Linear temporal logic, Initialization, Computer science, Satisfiability, Abstraction model checking, Interval temporal logic, Temporal logic, Theoretical computer science, Computation tree logic, Model checking
Related Organizations
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue