Propositional Dynamic Logic with Quantification over Regular Computation Sequences

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Propositional Dynamic Logic with Quantification over Regular Computation Sequences

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Propositional Dynamic Logic with Quantification over Regular Computation Sequences

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2022

Kód důvěrnosti údajů

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

Název statě ve sborníku

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

—

Počet stran výsledku

15

Strana od-do

301-315

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Deerfield Beach / Virtual

Datum konání akce

10. 1. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—