Preservation theorems hold for all lattice semirings but fail for tropical, Viterbi, Łukasiewicz, and natural semirings, while existential preservation holds on finite interpretations for lattices unlike the Boolean case.
Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science
6 Pith papers cite this work. Polarity classification is still indexing.
citation-role summary
citation-polarity summary
verdicts
UNVERDICTED 6roles
background 2representative citing papers
Efficient priority minimization for deterministic parity automata with don't care words is possible via a general result; WDBA have unique minimal forms under trivial right-congruence don't cares with a congruence characterization, but the informative right-congruence class has no unique minimal and
SCAN algorithm extended to compute witnesses for second-order quantifiers alongside quantifier elimination on clause sets.
Obligation properties in LTLf+ admit a direct symbolic translation to deterministic weak automata, enabling linear-time synthesis via DWA games with effectiveness comparable to LTLf.
Provides complexity results for the constrained existence problem of five equilibrium notions in multiplayer graph games.
Sure-almost-sure and sure-limit-sure problems for fixed and bounded window mean-payoff in MDPs are in P and NP ∩ coNP respectively.
citing papers explorer
-
Preservation Theorems in Semiring Semantics
Preservation theorems hold for all lattice semirings but fail for tropical, Viterbi, Łukasiewicz, and natural semirings, while existential preservation holds on finite interpretations for lattices unlike the Boolean case.
-
On Minimization and Learning of Deterministic $\omega$-Automata in the Presence of Don't Care Words
Efficient priority minimization for deterministic parity automata with don't care words is possible via a general result; WDBA have unique minimal forms under trivial right-congruence don't cares with a congruence characterization, but the informative right-congruence class has no unique minimal and
-
Computing Witnesses Using the SCAN Algorithm
SCAN algorithm extended to compute witnesses for second-order quantifiers alongside quantifier elimination on clause sets.
-
Symbolic Synthesis for LTLf+ Obligations
Obligation properties in LTLf+ admit a direct symbolic translation to deterministic weak automata, enabling linear-time synthesis via DWA games with effectiveness comparable to LTLf.
-
Equilibria in Multiplayer Graph Games: An Algorithmic Study
Provides complexity results for the constrained existence problem of five equilibrium notions in multiplayer graph games.
-
Sure-almost-sure and Sure-limit-sure Window Mean Payoff in Markov Decision Processes
Sure-almost-sure and sure-limit-sure problems for fixed and bounded window mean-payoff in MDPs are in P and NP ∩ coNP respectively.