Name
Abstract | ||
|---|---|---|
We consider an extension of linear-time temporal logic (LTL) with constraints inter- preted over a concrete domain. We use a new automata-theoretic technique to show pspace decidability of the logic for the constraint systems (Z,<,=) and (N,<,=). Along the way, we give an automata-theoretic proof of a result of (1) when the constraint system satisfies the completion property. Our decision procedures extend easily to handle extensions of the logic with past-time operators and constants, as well as an extension of the temporal language itself to monadic second order logic. Finally we show that the logic becomes undecidable when one considers constraint systems that allow a counting mechanism. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1016/j.ic.2006.09.006 | Foundations of Software Technology and Theoretical Computer Science |
Keywords | DocType | Volume |
logics of space and time,constraint system,temporal logic,automata-theoretic approach,pspace decidability,new automata-theoretic technique,linear-time temporal logic,concrete domain,model-checking,constraint ltl,satisfiability,model checking | Conference | 205 |
Issue | ISSN | ISBN |
3 | Information and Computation | 3-540-00225-1 |
Citations | PageRank | References |
37 | 1.24 | 52 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Stéphane Demri | 1 | 832 | 60.65 |
| Deepak D'souza | 2 | 239 | 17.90 |