ArticleJCSS16: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) K (Marcel Lippmann verschob die Seite En nach ArticleJCSS16) |
Claudia Carapelle (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
Zeile 10: | Zeile 10: | ||
|Year=2016 | |Year=2016 | ||
|Journal=Journal of Computer and System Sciences | |Journal=Journal of Computer and System Sciences | ||
|Volume=82 | |||
|Number=5 | |||
|Pages=826 - 855 | |||
|Publisher=Elsevier | |||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
Zeile 17: | Zeile 21: | ||
|Projekt=QuantLA | |Projekt=QuantLA | ||
|Forschungsgruppe=Automatentheorie | |Forschungsgruppe=Automatentheorie | ||
|BibTex=@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 " | |||
} | |||
}} | }} |
Version vom 21. April 2016, 14:04 Uhr
Satisfiability of ECTL* with Constraints
Claudia CarapelleClaudia Carapelle, Alexander KartzowAlexander Kartzow, Markus LohreyMarkus Lohrey
Claudia Carapelle, Alexander Kartzow, Markus Lohrey
Satisfiability of ECTL* with Constraints
Journal of Computer and System Sciences, 82(5):826 - 855, to appear
Satisfiability of ECTL* with Constraints
Journal of Computer and System Sciences, 82(5):826 - 855, to appear
- 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 "
}