The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties

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 past is a useful abstraction in specification. It allows one to ignore the complexity of system initialization in much the same ystem 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 centered on the problem of satisfiability checking of linear temporal logic (LTL) formulae with past operators. We show that bounded model checking techniques can be adapted to deal with bi-infinite time in temporal logic, without incurring in any performance loss. Our claims are supported by a tool, whose application to a case study shows that...

• Type: Conference
• Year: 2007
• Where: SIGSOFT
• Authors: Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro
• Keywords: Model Checking Techniques, Satisfiability Checking, SIGSOFT 2007, Software Engineering, Temporal Logic