First-order \(\mu\)-calculus over generic transition systems and applications to the situation calculus
From MaRDI portal
Publication:1706163
DOI10.1016/j.ic.2017.08.007zbMath1390.68462OpenAlexW2791668009MaRDI QIDQ1706163
Fabio Patrizi, Marco Montali, Giuseppe De Giacomo, Diego Calvanese
Publication date: 21 March 2018
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2017.08.007
verificationreasoning about actionssituation calculusfirst-order \(\mu\)-calculusinfinite transition systemsstate-bounded transition systems
Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items
Model checking Petri nets with names using data-centric dynamic systems, Non-terminating processes in the situation calculus, Are bundles good deals for first-order modal logic?, From DB-nets to Coloured Petri Nets with Priorities, Correctness Notions for Petri Nets with Identifiers, Situation calculus for controller synthesis in manufacturing systems with first-order state representation, Lifted model checking for relational MDPs, CTL* model checking for data-aware dynamic systems with arithmetic
Cites Work
- Bounded situation calculus action theories
- Model checking Petri nets with names using data-centric dynamic systems
- A lattice-theoretical fixpoint theorem and its applications
- Verification of Agent-Based Artifact Systems
- Action Theories over Generalized Databases with Equality Constraints
- LTL with the freeze quantifier and register automata
- Counterexample-guided abstraction refinement for symbolic model checking
- Description Logic Knowledge and Action Bases
- Decidability of DPDA equivalence
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
