Verification of agent-based artifact systems
From MaRDI portal
Abstract: Artifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycles, accounting respectively for the relational structure of the artifacts' states and their possible evolutions over time. In this paper we put forward artifact-centric multi-agent systems, a novel formalisation of artifact systems in the context of multi-agent systems operating on them. Differently from the usual process-based models of services, the semantics we give explicitly accounts for the data structures on which artifact systems are defined. We study the model checking problem for artifact-centric multi-agent systems against specifications written in a quantified version of temporal-epistemic logic expressing the knowledge of the agents in the exchange. We begin by noting that the problem is undecidable in general. We then identify two noteworthy restrictions, one syntactical and one semantical, that enable us to find bisimilar finite abstractions and therefore reduce the model checking problem to the instance on finite models. Under these assumptions we show that the model checking problem for these systems is EXPSPACE-complete. We then introduce artifact-centric programs, compact and declarative representations of the programs governing both the artifact system and the agents. We show that, while these in principle generate infinite-state systems, under natural conditions their verification problem can be solved on finite abstractions that can be effectively computed from the programs. Finally we exemplify the theoretical results of the paper through a mainstream procurement scenario from the artifact systems literature.
Recommendations
Cited in
(12)- First-order -calculus over generic transition systems and applications to the situation calculus
- Situation calculus for controller synthesis in manufacturing systems with first-order state representation
- Lifted model checking for relational MDPs
- From model completeness to verification of data aware processes
- Non-terminating processes in the situation calculus
- A three-value abstraction technique for the verification of epistemic properties in multi-agent systems
- Bounded situation calculus action theories
- Progression and verification of situation calculus agents with bounded beliefs
- Model checking Petri nets with names using data-centric dynamic systems
- Two-stage agent program verification
- Standard type soundness for agents and artifacts
- Model checking auctions as artifact systems: decidability via finite abstraction
This page was built for publication: Verification of agent-based artifact systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2925412)
