Browse wiki

From International Center for Computational Logic
We extend the propositional dynamic logic We extend the propositional dynamic logic PDL of Fischer and Ladner with a restricted kind of recursive programs using the formalism of visibly pushdown automata (Alur, Madhusudan 2004). We show that the satisfiability problem for this extension remains decidable, generalising known decidability results for extensions of PDL by non-regular programs. Our decision procedure establishes a 2- ExpTime upper complexity bound, and we prove a matching lower bound that applies already to rather weak extensions of PDL with non-regular programs. Thus, we also show that such extensions tend to be more complex than standard PDL.tend to be more complex than standard PDL.  +
Carsten Lutz +, C. Löding +  und O. Serre +
@article{ LoeLuSe-JLAP-07,
  author = {C. {L\"oding} and C. {Lutz} and O. {Serre}},
  journal = {Journal of Logic and Algebraic Programming},
  pages = {51--69},
  title = {Propositional Dynamic Logic with Recursive Programs},
  volume = {73},
  year = {2007},
}
Article  +
LoeLuSe.pdf  +
Journal of Logic and Algebraic Programming  +
51-69  +
C. Löding, Carsten Lutz, O. Serre<br/&gC. Löding, Carsten Lutz, O. Serre<br/> '''[[LATPub357|Propositional Dynamic Logic with Recursive Programs]]''' <br/>__NOTOC__Journal of Logic and Algebraic Programming, 73:51-69, 2007<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[LATPub357|Details]] <span class="fas fa-chevron-right" style="font-size: 85%; margin-left: 2ex; "></span> [[Media:LoeLuSe.pdf|Download]]ia:LoeLuSe.pdf|Download]]  +
C. Löding, Carsten Lutz, O. Serre<br/&gC. Löding, Carsten Lutz, O. Serre<br/> '''[[LATPub357/en|Propositional Dynamic Logic with Recursive Programs]]''' <br/>__NOTOC__Journal of Logic and Algebraic Programming, 73:51-69, 2007<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[LATPub357|Details]] <span class="fas fa-chevron-right" style="font-size: 85%; margin-left: 2ex;" ></span> [[Media:LoeLuSe.pdf|Download]]ia:LoeLuSe.pdf|Download]]  +
Propositional Dynamic Logic with Recursive Programs  +
article  +
73  +
2007  +
Anzeigetitel„Anzeigetitel <span style="font-size:small;">(Display title of)</span>“ ist ein softwareseitig fest definiertes Attribut, das einen eindeutigen Anzeigetitel zu einem Objekt speichert und ihm zuweist. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Propositional Dynamic Logic with Recursive Programs  +
Zuletzt geändert„Zuletzt geändert <span style="font-size:small;">(Modification date)</span>“ ist ein softwareseitig fest definiertes Attribut, das das Datum der letzten Änderung einer Seite speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
25. März 2015, 14:34:05  +
Hat Abfrage„Hat Abfrage <span style="font-size:small;">(Has query)</span>“ ist ein softwareseitig fest definiertes Attribut, das die Metainformationen einer Abfrage als <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">Subobjekt</a> speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.