Bounded Reachability for Temporal Logic over Constraint Systems
Logic in Computer Science
2010-04-21 v3
Abstract
We present CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. Even for decidable constraint systems, satisfiability and Model Checking problem of such logic can be undecidable. We introduce suitable restrictions and assumptions that are shown to make the satisfiability problem for the extended logic decidable. Moreover for a large class of constraint systems we propose an encoding that realize an effective decision procedure for the Bounded Reachability problem.
Keywords
Cite
@article{arxiv.1004.1077,
title = {Bounded Reachability for Temporal Logic over Constraint Systems},
author = {Marcello M. Bersani and Achille Frigeri and Angelo Morzenti and Matteo Pradella and Matteo Rossi and Pierluigi San Pietro},
journal= {arXiv preprint arXiv:1004.1077},
year = {2010}
}