188 results found
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.
Grandi F, Lange M, Lomuscio A, 2015, Message from Programme Co-chairs
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.
Griesmayer A, Lomuscio A, 2013, Model checking distributed systems against temporal-epistemic specifications, Pages: 130-145, ISSN: 0302-9743
Concurrency and message reordering are two main causes for the state-explosion in distributed systems with asynchronous communication. We study this domain by analysing ABS, an executable modelling language for object-based distributed systems and present a symbolic model checking methodology for verifying ABS programs against temporal-epistemic specifications. Specifically, we show how to map an ABS program into an ISPL program for verification with MCMAS, a model checker for multi-agent systems. We present a compiler implementing the formal map, exemplify the methodology on a mesh network use case and report experimental results. © 2013 IFIP International Federation for Information Processing.
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.
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
De Giacomo G, Felli P, Lomuscio A, 2012, Synthesizing agent protocols from LTL specifications against multiple partially-observable environments, Pages: 457-466
We consider the problem of synthesizing an agent protocol satisfying LTL specifications for multiple, partially-observable environments. We present a sound and complete procedure for solving the synthesis problem in this setting and show it is computationally optimal from a theoretical complexity standpoint. While this produces perfect-recall, hence unbounded, strategies we show how to transform these into agent protocols with bounded number of states. Copyright © 2012, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
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.
Lomuscio A, Penczek W, 2012, Symbolic model checking for temporal-epistemic logic, Pages: 172-195, ISSN: 0302-9743
We survey some of the recent work in verification via symbolic model checking of temporal-epistemic logic. Specifically, we discuss OBDD-based and SAT-based approaches for epistemic logic built on discrete and real-time branching time temporal logic. The underlying semantical model considered throughout is the one of interpreted system, suitably extended whenever necessary. © 2012 Springer-Verlag Berlin Heidelberg.
Marek Sergot's technical contributions range over different subjects. He has developed a series of novel ideas and formal methods bridging different research domains, such as artificial intelligence, computational logic, philosophical logic, legal theory, artificial intelligence and law, multi-agent systems and bioinformatics. By combining his background in logic and computing with his interest in the law, deontic logic, action, and related areas, and applying to all his capacity to understand the subtleties of social interactions and normative reasoning, Marek has been able to open new directions of research, and has been a reference, an inspiration, and a model for many researchers in the many fields in which he has worked. © 2012 Springer-Verlag Berlin Heidelberg.
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.