Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

+44 (0)20 7594 8414a.lomuscio Website

 
 
//

Location

 

504Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

187 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.

Conference paper

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

Conference paper

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.

Conference paper

Grandi F, Lange M, Lomuscio A, 2015, Message from Programme Co-chairs

Conference paper

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.

Conference paper

, 2015,

Conference paper

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

Conference paper

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.

Journal article

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.

Conference paper

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.

Conference paper

Cermak P, Lomuscio A, Mogavero F, Murano Aet 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.

Journal article

, 2014,

Conference paper

, 2014,

Conference paper

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

Journal article

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.

Conference paper

Belardinelli F, Lomuscio A, Patrizi F, 2014, Verification of Agent-based Artifact Systems, Journal of Artificial Intelligence Research, Vol: 51, Pages: 333-376

Journal article

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.

Conference paper

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.

Conference paper

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.

Conference paper

Lomuscio A, Strulo B, Walker N, Wu Pet al., 2013, ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS, INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, Vol: 24, Pages: 419-444, ISSN: 0129-0541

Journal article

, 2013,

Journal article

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.

Journal article

, 2013,

Conference paper

Belardinelli F, Lomuscio A, 2013, Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems, Publisher: AAAI Press, Pages: 725-731

Conference paper

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.

Conference paper

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.

Conference paper

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.

Conference paper

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.

Conference paper

Barker S, Jones AJI, Kakas A, Kowalski RA, Lomuscio A, Miller R, Muggleton S, Sartor Get al., 2012, The scientific contribution of marek sergot, Pages: 4-11, ISSN: 0302-9743

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.

Conference paper

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.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: id=00306568&limit=30&person=true&page=2&respub-action=search.html