Propositional Dynamic Logic with Quantification over Regular Computation Sequences

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F22%3A00553385" target="_blank" >RIV/67985807:_____/22:00553385 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-030-93100-1_19" target="_blank" >http://dx.doi.org/10.1007/978-3-030-93100-1_19</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-93100-1_19" target="_blank" >10.1007/978-3-030-93100-1_19</a>

Result language
angličtina
Original language name
Propositional Dynamic Logic with Quantification over Regular Computation Sequences
Original language description
We extend test-free regular propositional dynamic logic with operators expressing combinations of existential and universal quantifiers quantifying over computation sequences represented by a given regular expression and states accessible via these computation sequences. This extended language is able to express that there is a computation sequence represented by a given regular expression that leads only to states where a given formula is satisfied, or that for all computation sequences represented by a given regular expression there is a state accessible via the computation sequence where a given formula is satisfied. Such quantifier combinations are essential in expressing, for instance, that a given non-deterministic finite automaton accepts all words of a given regular language or that there is a specific sequence of actions instantiating a plan expressed by a regular expression that is guaranteed to accomplish a certain goal. The existential-universal quantifier combination is modelled by neighborhood functions. We prove that a rich fragment of our logic is decidable and EXPTIME -complete by embedding the fragment into deterministic propositional dynamic logic.
Czech name
—
Czech description
—

Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Logical Foundations of Computer Science. International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10–13, 2022, Proceedings
ISBN
978-3-030-93099-8
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
301-315
Publisher name
Springer
Place of publication
Cham
Event location
Deerfield Beach / Virtual
Event date
Jan 10, 2022
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)