The Modal μ-Calculus is an extension of Modal Logic with two operators for least (μ) and greatest (ν) fixpoints of monotone functions. This logic is widely used as a tool for specification and verification of computer systems. We show that, on transitive structures, every formula of the μ-Calculus is equivalent to a Büchi automaton.
The transitive $mu$-Calculus is B"uchi definable,
LENZI, Giacomo
2006
Abstract
The Modal μ-Calculus is an extension of Modal Logic with two operators for least (μ) and greatest (ν) fixpoints of monotone functions. This logic is widely used as a tool for specification and verification of computer systems. We show that, on transitive structures, every formula of the μ-Calculus is equivalent to a Büchi automaton.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
