Sciweavers

Share
SIGSOFT
2007
ACM

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

10 years 8 months ago
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...
Matteo Pradella, Angelo Morzenti, Pierluigi San Pi
Added 20 Nov 2009
Updated 20 Nov 2009
Type Conference
Year 2007
Where SIGSOFT
Authors Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro
Comments (0)
books