Authors
Matteo Pradella, Pierluigi San Pietro, Paola Spoletini, Angelo Morzenti
Publication date
2003/12
Journal
ATVA03: 1st Workshop on Automated Technology for Verification and Analysis
Description
LTL (Linear Temporal Logic) has become the standard language for linear-time model checking. LTL has only future operators, while it is widely accepted that many specifications are easier, shorter and more intuitive when also past operators are allowed. Moreover, adding past operators does not increase the complexity of LTL model checking, which is still PSPACE-complete. However, model checking past formulae is not very easy in practice, and it is not clear how to efficiently reuse existing model checkers like SPIN. In this paper, we propose a reasonably efficient approach to model (and satisfiability) checking of LTL-with-past formulae in a quasi-separate normal form, which occurs very often in applications.
Total citations
Scholar articles
M Pradella, P San Pietro, P Spoletini, A Morzenti - ATVA03: 1st Workshop on Automated Technology for …, 2003