191 results found
Lomuscio A, Michaliszyn J, 2015, Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions
The Epistemic Halpern-Shoham logic (EHS) is a temporal-epistemic logic thatcombines the interval operators of the Halpern-Shoham logic with epistemicmodalities. The semantics of EHS is based on interpreted systems whoselabelling function is defined on the endpoints of intervals. We show that thisdefinition can be generalised by allowing the labelling function to be based onthe whole interval by means of regular expressions. We prove that all thepositive results known for EHS, notably the attractive complexity of its modelchecking problem for some of its fragments, still hold for its generalisation.We also propose the new logic EHSre which operates on standard Kripkestructures and has expressive power equivalent to that of EHS with regularexpressions. We compare the expressive power of EHSre with standard temporallogics.
Lomuscio AR, Kouvaros P, Verifying Emergent Properties of Swarms, Twenty-Fourth International Conference on Artificial Intelligence (IJCAI15), Publisher: AAAI Press, Pages: 1083-1089
Lomuscio AR, Paquet H, 2015, Verification of Multi-Agent Systems via SDD-based Model Checking, Proceedings of the 14th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS15), Publisher: IFAAMAS Press, Pages: 1713-1714
Lomuscio AR, Michaliszyn J, 2015, Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions, 14th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS15), Publisher: IFAAMAS Press, Pages: 189-198
We develop the theoretical foundations of a predicate ab-straction methodology for the verification of multi-agent sys-tems. We put forward a specification language based onepistemic logic and a weak variant of the logic ATL inter-preted on a three-valued semantics. We show that the modelchecking problem for multi-agent systems in this setting istractable by giving a provably correct procedure which ad-mits a PTime bound. We give a constructive techniquefor generating abstract approximations of concrete multi-agent systems models and show that the truth values arepreserved between abstract and concrete models. We evalu-ate the effectiveness of the methodology on a variant of thebit-transmission problem.
Lomuscio AR, Kouvaros P, 2015, A Counter Abstraction Technique for the Verification of Robot Swarms., Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI15), Publisher: AAAI, Pages: 2081-2088
We study parameterised verification of robot swarmsagainst temporal-epistemic specifications. We relaxsome of the significant restrictions assumed in the lit-erature and present a counter abstraction approach thatenable us to verify a potentially much smaller abstractmodel when checking a formula on a swarm of any size.We present an implementation and discuss experimen-tal results obtained for the alpha algorithm for robotswarms
Lomuscio AR, Cermak P, Murano A, Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications, Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI15), Publisher: AAAI Press, Pages: 2038-2044
Strategy Logic (SL) has recently come to the fore as a usefulspecification language to reason about multi-agent systems.Its one-goal fragment, or SL[1G], is of particular interest asit strictly subsumes widely used logics such as ATL*, whilemaintaining attractive complexity features. In this paper weput forward an automata-based methodology for verifyingand synthesising multi-agent systems against specificationsgiven in SL[1G]. We show that the algorithm is sound andoptimal from a computational point of view. A key featureof the approach is that all data structures and operations onthem can be performed on BDDs. We report on a BDD-basedmodel checker implementing the algorithm and evaluate itsperformance against a number of scalable scenarios.
Lomuscio A, Colombetti M, 2015, QLB: A quantified logic for belief, Pages: 71-85, ISSN: 0302-9743
© 2015, Lecture Notes in Computer Science. All rights reserved. This paper describes QLB, a quantified logic of belief that is a possible extension of the modal system KD45n to predicate level. The main features of QLB are that: (i) it is allowed to quantify over the agents of belief; (ii) the belief operator can be indexed by any term of the formal language; (iii) terms are not rigid designators, but are interpreted contextually; (iv) automatic theorem proving is possible in QLB (but it is not presented in this paper). QLB is constructed as a partial logic with a monotonic semantics on ordered sets, and its semantic theorems are defined as the formulae that are sometimes true and never false.
Belardinelli F, Grossi D, Lomuscio A, 2015, Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems, Publisher: AAAI Press, Pages: 854-860
, 2015, 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, Kassel, Germany, September 23-25, 2015, Publisher: IEEE Computer Society
Belardinelli F, Lomuscio A, Patrizi F, 2014, Verification of agent-based artifact systems, The Journal of Artificial Intelligence Research, Vol: 51, ISSN: 1076-9757
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, we give a semantics that 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 expressed 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 identify a noteworthy class of systems that admit bisimilar, finite abstractions. It follows that we can verify these systems by investigating their finite abstractions; we also show that the corresponding model checking problem 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. We exemplify the theoretical results here pursued through a mainstream procurement scenario from the artifact systems literature.
Lomuscio AR, Michaliszyn J, Model Checking Unbounded Artifact-Centric Systems, 14th International Conference on Principles of Knowledge Representation and Reasoning (KR14), Publisher: AAAI Press, Pages: 488-497
Artifact-centric systems are a recent paradigm for represent-ing and implementing business processes. We present furtherresults on the verification problem of artifact-centric systemsspecified by means of FO-CTL specifications. While the gen-eral problem is known to be undecidable, results in the lit-erature prove decidability for artifact systems with infinitedomains under boundedness and conditions such as unifor-mity. We here follow a different approach and investigate thegeneral case with infinite domains. We show decidability ofthe model checking problem for the class of artifact-centricsystems whose database schemas consist of a single unaryrelation, and we show that that the problem is undecidable ifartifact systems are defined by using one binary relation ortwo unary relations.
Lomuscio AR, An abstraction technique for the verification of multi-agent systems against ATL specifications, 14th International Conference on Principles of Knowledge Representation and Reasoning (KR14), Publisher: AAAI Press, Pages: 428-437
We introduce an abstraction methodology for the verificationof multi-agent systems against specifications expressed inalternating-time temporal logic (ATL). Inspired by methodolo-gies such as predicate abstraction, we define a three-valuedsemantics for the interpretation of ATL formulas on concurrentgame structures and compare it to the standard two-valued se-mantics. We define abstract models and establish preservationresults on the three-valued semantics between abstract modelsand their concrete counterparts. We illustrate the methodologyon the large state spaces resulting from a card game.
Cermak P, Lomuscio A, Mogavero F, et al., 2014, MCMAS-SLK: A model checker for the verification of strategy logic specifications, Lecture Notes in Computer Science, Vol: 8559, Pages: 525-532, ISSN: 0302-9743
Model checking has come of age. A number of techniques are increasingly used in industrial setting to verify hardware and software systems, both against models and concrete implementations. While it is generally accepted that obstacles still remain, notably handling infinite state systems efficiently, much of current work involves refining and improving existing techniques such as predicate abstraction. © 2014 Springer International Publishing.
Lomuscio AR, 2014, Advances in symbolic model checking for multi-agent systems
Gonzalez P, Griesmayer A, Lomuscio A, 2014, Model Checking GSM-Based Multi-Agent Systems, SERVICE-ORIENTED COMPUTING - ICSOC 2013 WORKSHOPS, Vol: 8377, Pages: 54-68, ISSN: 0302-9743
Lomuscio AR, Michaliszyn J, 2014, Decidability of model checking multi-agent systems against a class of EHS specifications, 21st European Conference on Artificial Intelligence (ECAI), Publisher: IOS Press, Pages: 543-548, ISSN: 0922-6389
We define and illustrate the expressiveness of the ABL¯fragment of the Epistemic Halpern–Shoham Logic as a specificationlanguage for multi-agent systems. We consider the model checkingproblem for systems against specifications given in the logic.We show its decidability by means of a novel technique that maybe reused in other contexts for showing decidability of other logicsbased on intervals.
, 2014, Service-Oriented Computing - ICSOC 2013 Workshops - CCSA, CSB, PASCEB, SWESE, WESOA, and PhD Symposium, Berlin, Germany, December 2-5, 2013. Revised Selected Papers, Publisher: Springer
Belardinelli F, Lomuscio A, Patrizi F, 2014, Verification of Agent-based Artifact Systems, Journal of Artificial Intelligence Research, Vol: 51, Pages: 333-376
Lomuscio A, Moss LS, Ovchinnikova E, et al., 2014, Tutorials., Publisher: AAAI Press
Kouvaros P, Lomuscio A, 2013, A cutoff technique for the verification of parameterised interpreted systems with parameterised environments, Twenty-Third Joint Conference on Artificial Intelligence, Publisher: AAAI Press / International Joint Conferences on Artificial Intelligence, Pages: 2013-2019, ISSN: 1045-0823
We put forward a cutoff technique for determining the number of agents that is sufficient to consider when checking temporal-epistemic specifications on a system of any size. We identify a special class of interleaved interpreted systems for which we give a parameterised semantics and an abstraction methodology. This enables us to overcome the significant limitations in expressivity present in the state-of-the-art. We present an implementation and discuss experimental results.
Lomuscio AR, Michaliszyn J, 2013, An epistemic Halpern-Shoham logic, Pages: 1010-1016, ISSN: 1045-0823
We define a family of epistemic extensions of Halpern-Shoham logic for reasoning about temporal-epistemic properties of multi-agent systems. We exemplify their use and study the complexity of their model checking problem. We show a range of results ranging from PTIME to PSPACE-hard depending on the logic considered.
Lomuscio A, Strulo B, Walker N, et al., 2013, ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS, INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, Vol: 24, Pages: 419-444, ISSN: 0129-0541
Kouvaros P, Lomuscio A, 2013, Automatic verification of parameterised interleaved multi-agent systems, 12th International Conference on Autonomous Agents and Multiagent Systems 2013, AAMAS 2013, Vol: 2, Pages: 861-868
A key problem in verification of multi-agent systems by model checking concerns the fact that the state-space of the system grows exponentially with the number of agents present. This often makes practical model checking unfeasible whenever the system contains more than a few agents. In this paper we put forward a technique to establish a cutoff result, thereby showing that systems with an arbitrary number of agents can be verified by checking a single system consisting of a number of agents equal to the cutoff of the system. While this problem is undecidable in general, we here define a class of parameterised interpreted systems and a parameterised temporal-epistemic logic for which the result can be shown. We exemplify the theoretical results on a robotic example and present an implementation of the technique as an extension of MCMAS, an open-source model checker for multi-agent systems. Copyright © 2013, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
Griesmayer A, Lomuscio A, 2013, Model Checking Distributed Systems against Temporal-Epistemic Specifications, Joint IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems (33rd FMOODS/15th FORTE) Held as Part of the 8th International Federated Conference on Distributed Computing Techniques (DisCoTec), Publisher: SPRINGER-VERLAG BERLIN, Pages: 130-145, ISSN: 0302-9743
Belardinelli F, Lomuscio A, 2013, Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems, Publisher: AAAI Press, Pages: 725-731
Kouvaros P, Lomuscio A, 2013, Automatic verification of parameterised multi-agent systems., Publisher: IFAAMAS, Pages: 861-868
Lomuscio A, Pinchinat S, Schlingloff H, 2013, VaToMAS - Verification and Testing of Multi-Agent Systems (Dagstuhl Seminar 13181)., Dagstuhl Reports, Vol: 3, Pages: 151-187
Gonzalez P, Griesmayer A, Lomuscio A, 2012, Verifying GSM-based business artifacts, Pages: 25-32
Business artifacts allow to manage operations of business processes by capturing the key concepts and relevant information to guide their work flow. The Guard-Stage- Milestone (GSM) meta-model is a novel formalism for designing business artifacts that features declarative description of the intended behaviour without requiring an explicit specification of the control flow. Its concept of hierarchical structures of stages and explicit rules for the fulfilment of their guards and milestones supports the designing process but poses a challenge for formal verification. We show here how to approach the verification problem by developing a symbolic representation amenable to model checking. The feasibility of the approach is demonstrated by presenting a case study on the direct verification of a GSM model using a tool implementation. © 2012 IEEE.
Belardinelli F, Gonzalez P, Lomuscio A, 2012, Automated verification of quantum protocols using MCMAS, Tenth Workshop on Quantitative Aspects of Programming Languages QAPL 2012, Publisher: arXiv, Pages: 48-62
We present a methodology for the automated verification of quantum protocols using MCMAS, a symbolic model checker for multi-agent systems The method is based on the logical framework developed by D'Hondt and Panangaden for investigating epistemic and temporal properties, built on the model for Distributed Measurement-based Quantum Computation (DMC), an extension of the Measurement Calculus to distributed quantum systems. We describe the translation map from DMC to interpreted systems, the typical formalism for reasoning about time and knowledge in multi-agent systems. Then, we introduce dmc2ispl, a compiler into the input language of the MCMAS model checker. We demonstrate the technique by verifying the Quantum Teleportation Protocol, and discuss the performance of the tool.
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.