Formula size games for modal logic and mu-calculus

Tutkimustuotos: ArtikkeliScientificvertaisarvioitu

1 Sitaatiot (Scopus)
24 Lataukset (Pure)

Abstrakti

We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic FO and (basic) modal logic ML⁠. We also present a version of the game for the modal μ-calculus Lμ and show that FO is also non-elementarily more succinct than Lμ⁠.
AlkuperäiskieliEnglanti
Artikkeliexz025
Sivut1311-1344
JulkaisuJOURNAL OF LOGIC AND COMPUTATION
Vuosikerta29
Numero8
DOI - pysyväislinkit
TilaJulkaistu - 2019
OKM-julkaisutyyppiA1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä

Tutkimusalat

  • Succinctness
  • bisimulation invariant first-order logic
  • formula size game
  • modal logic
  • modal mu-calculus
  • succinctness

Julkaisufoorumi-taso

  • Jufo-taso 2

Sormenjälki

Sukella tutkimusaiheisiin 'Formula size games for modal logic and mu-calculus'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä