Bounded game-theoretic semantics for modal mu-calculus

Lauri Hella, Antti Kuusisto, Raine Rönnholm

Tutkimustuotos: ArtikkeliScientificvertaisarvioitu

18 Lataukset (Pure)

Abstrakti

We introduce a new game-theoretic semantics (GTS) for the modal mu-calculus. Our so-called bounded GTS replaces parity games with alternative evaluation games where only finite paths arise; infinite paths are not needed even when the considered transition system is infinite. The novel games offer alternative approaches to various constructions in the framework of the mu-calculus. While our main focus is introducing the new GTS, we also consider some applications to demonstrate its uses. For example, we consider a natural model transformation procedure that reduces model checking games to checking a single, fixed formula in the constructed models. We also use the GTS to identify new alternative variants of the mu-calculus, including close variants of the logic with PTime model checking; variants with iteration limited to finite ordinals; and other systems where the semantic or syntactic specification of the mu-calculus has been modified in a natural way suggested by the GTS.

AlkuperäiskieliEnglanti
Artikkeli104882
Sivumäärä19
JulkaisuInformation and Computation
Vuosikerta289
NumeroB
Varhainen verkossa julkaisun päivämäärä2022
DOI - pysyväislinkit
TilaJulkaistu - 2022
OKM-julkaisutyyppiA1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä

Julkaisufoorumi-taso

  • Jufo-taso 2

!!ASJC Scopus subject areas

  • Theoretical Computer Science
  • Information Systems
  • Computer Science Applications
  • Computational Theory and Mathematics

Sormenjälki

Sukella tutkimusaiheisiin 'Bounded game-theoretic semantics for modal mu-calculus'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä