Version vom 23. März 2016, 11:24 Uhr

Satisfiability of CTL* with constraints

Claudia CarapelleClaudia Carapelle, Alexander KartzowAlexander Kartzow, Markus LohreyMarkus Lohrey

DOI Link

Claudia Carapelle, Alexander Kartzow, Markus Lohrey
Satisfiability of CTL* with constraints
Concurrency Theory: 24th International Conference, CONCUR 2013, volume 8052 of LNCS, 455-469, 2013. Springer

Details
Bibtex

KurzfassungAbstract
We show that satisfiability for CTL* with equality-, order-, and modulo-constraints over the integers is decidable. Previously, decidability was only known for certain fragments of CTL*, e.g., the existential and positive fragments and EF.
Weitere Informationen unter:Further Information: Link
Projekt:Project: QuantLA
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-40184-8_32.

@Inbook{Carapelle2013,
author="Carapelle, Claudia
and Kartzow, Alexander
and Lohrey, Markus",
editor="D'Argenio, Pedro R.
and Melgratti, Hern{\'a}n",
chapter="Satisfiability of CTL* with Constraints",
title="CONCUR 2013 -- Concurrency Theory: 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings",
year="2013",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="455--469",
isbn="978-3-642-40184-8",
doi="10.1007/978-3-642-40184-8_32",
url="http://dx.doi.org/10.1007/978-3-642-40184-8_32"
}

@@ Zeile 2: / Zeile 2: @@
 |ErsterAutorVorname=Claudia
 |ErsterAutorNachname=Carapelle
 |FurtherAuthors=Alexander Kartzow; Markus Lohrey;
+}}
+{{Inproceedings
+|Referiert=1
+|Title=Satisfiability of CTL* with constraints
+|To appear=0
+|Year=2013
+|Booktitle=Concurrency Theory: 24th International Conference, CONCUR 2013
+|Pages=455-469
+|Publisher=Springer
+|Series=LNCS
+|Volume=8052
+}}
+{{Publikation Details
+|Abstract=We show that satisfiability for CTL* with equality-, order-, and modulo-constraints over the integers is decidable. Previously, decidability was only known for certain fragments of CTL*, e.g., the existential and positive fragments and EF.
+|Link=http://dx.doi.org/10.1007/978-3-642-40184-8_32
+|DOI Name=10.1007/978-3-642-40184-8_32
+|Projekt=QuantLA
+|Forschungsgruppe=Automatentheorie
+|BibTex=@Inbook{Carapelle2013,
+author="Carapelle, Claudia
+and Kartzow, Alexander
+and Lohrey, Markus",
+editor="D'Argenio, Pedro R.
+and Melgratti, Hern{\'a}n",
+chapter="Satisfiability of CTL* with Constraints",
+title="CONCUR 2013 -- Concurrency Theory: 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings",
+year="2013",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="455--469",
+isbn="978-3-642-40184-8",
+doi="10.1007/978-3-642-40184-8_32",
+url="http://dx.doi.org/10.1007/978-3-642-40184-8_32"
+}
 }}
 {{Article
@@ Zeile 10: / Zeile 45: @@
 |Year=2016
 |Journal=Journal of Computer and System Sciences
-}}
-{{Publikation Details
-|Abstract=We show that satisfiability and finite satisfiability for ECTL* with equality-, order-, and modulo-constraints over Z 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 Z, the resulting logic becomes undecidable.
-|Link=http://authors.elsevier.com/sd/article/S002200001600012X
-|DOI Name=10.1016/j.jcss.2016.02.002
-|Projekt=QuantLA
-|Forschungsgruppe=Automatentheorie
 }}

ArticleJCSS16: Unterschied zwischen den Versionen

Version vom 23. März 2016, 11:24 Uhr

Satisfiability of CTL* with constraints

Claudia CarapelleClaudia Carapelle, Alexander KartzowAlexander Kartzow, Markus LohreyMarkus Lohrey