First-order μ-calculus over generic transition systems and applications to the situation calculus

摘要: Abstract We consider μ L , a and p three variants of the first-order μ-calculus studied in verification data-aware processes, that differ form quantification on objects across states. Each these logics has distinct notion bisimulation. show notions collapse for generic dynamic systems, which include all state-based systems specified using logical formalism, e.g., situation calculus. Hence, such have same expressive power. also that, when system stores only bounded number each state (e.g., calculus action theories), finite abstraction can be constructed is faithful (the most general variant), yielding decidability verification. This contrasts with undecidability ltl notably implies cannot captured by .