Satisfiability of ECTL* with Constraints

Claudia CarapelleClaudia Carapelle, Alexander KartzowAlexander Kartzow, Markus LohreyMarkus Lohrey

ISSN: 0022-0000
DOI Link

Claudia Carapelle, Alexander Kartzow, Markus Lohrey
Satisfiability of ECTL* with Constraints
Journal of Computer and System Sciences, 82(5):826 - 855, 2016

Details
Bibtex

KurzfassungAbstract
We show that satisfiability and finite satisfiability for ECTL* with equality-, order-, and modulo-constraints over the integers are decidable. Since ECTL* is a proper extension of CTL* this greatly improves the previously known decidability results for certain fragments of CTL*, e.g., the existential and positive fragments and EF. We also show that our choice of local constraints is necessary for the result in the sense that, if we add the possibility to state non-local constraints over the integers, the resulting logic becomes undecidable.
Weitere Informationen unter:Further Information: Link
Projekt:Project: QuantLA
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{Carapelle2016826,
title = "Satisfiability of ECTL$^*$ with constraints ",
journal = "Journal of Computer and System Sciences ",
volume = "82",
number = "5",
pages = "826 - 855",
year = "2016",
note = "",
issn = "0022-0000",
doi = "http://dx.doi.org/10.1016/j.jcss.2016.02.002",
url = "http://www.sciencedirect.com/science/article/pii/S002200001600012X",
author = "Claudia Carapelle and Alexander Kartzow and Markus Lohrey",
keywords = "Temporal logics with integer constraints",
keywords = "ECTL*",
keywords = "Monadic second-order logic with the bounding quantifier "
}