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

Belardinelli F, Lomuscio A, Malvone A, An abstraction-based method for verifying strategic properties in multi-agent systems with imperfect information, Thirty-Third AAAI Conference on Artificial Intelligence, Publisher: Association for the Advancement of Artificial Intelligence

We investigate the verification of Multi-agent Systemsagainst strategic properties expressed in Alternating-timeTemporal Logic under the assumptions of imperfect informa-tion and perfect recall. To this end, we develop a three-valuedsemantics for concurrent game structures upon which we de-fine an abstraction method. We prove that concurrent gamestructures with imperfect information admit perfect informa-tion abstractions that preserve three-valued satisfaction. Fur-ther, we present a refinement procedure to deal with caseswhere the value of a specification is undefined. We illustratethe overall procedure in a variant of the Train Gate Controllerscenario under imperfect information and perfect recall.

Conference paper

Fu H, Ghosh A, Kopf J, 2018, Preface, Logic and Communication in Multi-Agent Systems, Publisher: WILEY, ISSN: 0167-7055

Conference paper

Lomuscio AR, Vardi MY, 2018, 4th International Workshop on Strategic Reasoning (SR 2016) Preface, SR 2016 : 4th International Workshop on Strategic Reasoning, Publisher: ACADEMIC PRESS INC ELSEVIER SCIENCE, Pages: 615-615, ISSN: 0890-5401

Conference paper

Čermák P, Lomuscio A, Mogavero F, Murano Aet al., 2018, Practical verification of multi-agent systems against Slk specifications, Information and Computation, Vol: 261, Pages: 588-614, ISSN: 0890-5401

We introduce Strategy Logic with Knowledge, a novel formalism to reason about knowledge and strategic ability in memoryless multi-agent systems with incomplete information. We exemplify its expressive power; we define the model checking problem for the logic and show that it is PSpace-complete. We propose a labelling algorithm for solving the verification problem that we show is amenable to symbolic implementation. We introduce Image 1, an extension of the open-source model checker MCMAS, implementing the proposed algorithm. We report the benchmarks obtained on a number of scenarios from the literature, including the dining cryptographers protocol.

Journal article

Lomuscio AR, Belardinelli F, malvone V, Approximating perfect recall when model checking strategic abilities, 16th International Conference on Principles of Knowledge Representation and Reasoning, Publisher: Association for the Advancement of Artificial Intelligence

We investigate the notion of bounded recall in the contextof model checkingATL∗andATLspecifications in multi-agent systems with imperfect information. We present a novelthree-valued semantics forATL∗, respectivelyATL, underbounded recall and imperfect information, and study the cor-responding model checking problems. Most importantly, weshow that the three-valued semantics constitutes an approxi-mation with respect to the traditional two-valued semantics.In the light of this we construct a sound, albeit partial, al-gorithm for model checking two-valued perfect recall via itsapproximation as three-valued bounded recall.

Conference paper

Lomuscio AR, akitunde M, maganti L, Pirovano Eet al., Reachability Analysis for Neural Agent-Environment Systems, 16th International Conference on Principles of Knowledge Representation and Reasoning, Publisher: Association for the Advancement of Artificial Intelligence

We develop a novel model for studying agent-environmentsystems, where the agents are implemented via feed-forwardReLU neural networks. We provide a semantics and developa method to verify automatically that no unwanted states arereached by the system during its evolution. We study severalreachability problems for the system, ranging from one-stepreachability, to fixed multi-step and arbitrary-step to studythe system evolution. We also study the decision problem ofwhether an agent, realised via feed-forward ReLU networkswill perform an action in a system run. Whenever possible,we give tight complexity bounds to decision problems intro-duced. We automate the various reachability problems stud-ied by recasting them as mixed-integer linear programmingproblems. We present an implementation and discuss the ex-perimental results obtained on a range of test cases.

Conference paper

Belardinelli F, Lomuscio A, Malvone V, Approximating Perfect Recall when Model Checking Strategic Abilities, Knowledge Representation and Reasoning

Conference paper

Belardinelli F, Lomuscio A, Murano A, Rubin Set al., Alternating-time temporal logic on finite traces, International Joint Conference on Artificial Intelligence, Pages: 77-83, ISSN: 1045-0823

© 2018 International Joint Conferences on Artificial Intelligence. All right reserved. We develop a logic-based technique to analyse finite interactions in multi-agent systems. We introduce a semantics for Alternating-time Temporal Logic (for both perfect and imperfect recall) and its branching-time fragments in which paths are finite instead of infinite. We study validities of these logics and present optimal algorithms for their model-checking problems in the perfect recall case.

Conference paper

Belardinelli F, Murano A, Lomuscio A, Rubin Set al., Decidable verification of multi-agent systems with bounded private actions, Autonomous Agents and Multiagent Systems, Pages: 1865-1867, ISSN: 1548-8403

Conference paper

Belardinelli F, Lomuscio A, Murano A, Rubin Set al., 2017, Verification of Multi-agent Systems with Imperfect Information and Public Actions, 16th Conference on Autonomous Agents and MultiAgent Systems

Conference paper

Belardinelli F, Kouvaros P, Lomuscio A, Parameterised verification of data-aware multi-agent systems, International Joint Conference on Artificial Intelligence, Pages: 98-104, ISSN: 1045-0823

We introduce parameterised data-aware multiagent systems, a formalism to reason about the temporal properties of arbitrarily large collections of homogeneous agents, each operating on an infinite data domain. We show that their parameterised verification problem is semi-decidable for classes of interest. This is demonstrated by separately addressing the unboundedness of the number of agents and the data domain. In doing so we reduce the parameterised model checking problem for these systems to that of parameterised verification for interleaved interpreted systems. We illustrate the expressivity of the formal model by modelling English auctions with an unbounded number of bidders on unbounded data.

Conference paper

Belardinelli F, Lomuscio A, Murano A, Rubin Set al., Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic, International Joint Conference on Artificial Intelligence

Conference paper

Hasani R, Haerle D, Baumgartner C, Lomuscio AR, Grosu Ret al., Compositional neural-network modeling of complex analog circuits, Proceedings of the 30th International Conference on Neural Networks, Publisher: IEEE

We introduce CompNN, a compositional method forthe construction of a neural-network (NN) capturing the dynamicbehavior of a complex analog multiple-input multiple-output(MIMO) system. CompNN first learns for each input/outputpair(i, j), a small-sized nonlinear auto-regressive neural networkwith exogenous input (NARX) representing the transfer-functionhij. The training dataset is generated by varying inputiof theMIMO, only. Then, for each outputj, the transfer functionshijare combined by a time-delayed neural network (TDNN) layer,fj.The training dataset forfjis generated by varying all MIMOinputs. The final output isf=(f1,...,fn). The NNs parame-ters are learned using Levenberg-Marquardt back-propagationalgorithm. We apply CompNN to learn an NN abstraction of aCMOS band-gap voltage-reference circuit (BGR). First, we learnthe NARX NNs corresponding to trimming, load-jump and line-jump responses of the circuit. Then, we recompose the outputsby training the second layer TDNN structure. We demonstratethe performance of our learned NN in the transient simulationof the BGR by reducing the simulation-time by a factor of 17compared to the transistor-level simulations. CompNN allows usto map particular parts of the NN to specific behavioral featuresof the BGR. To the best of our knowledge, CompNN is the firstmethod to learn the NN of an analog integrated circuit (MIMOsystem) in a compositional fashion.

Conference paper

Lomuscio AR, Qu H, Raimondi F, 2017, MCMAS: an open-source model checker for the verification of multi-agent systems, International Journal on Software Tools for Technology Transfer, ISSN: 1433-2779

We present MCMAS, a model checker for the verification of multi-agent systems. MCMAS supports efficient symbolic techniques for the verification of multi-agent systems against specifications representing temporal, epistemic and strategic properties. We present the underlying semantics of the specification language supported and the algorithms implemented in MCMAS, including its fairness and counterexample generation features. We provide a detailed description of the implementation. We illustrate its use by discussing a number of examples and evaluate its performance by comparing it against other model checkers for multi-agent systems on a common case study.

Journal article

Belardinelli F, Lomuscio A, Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect Information, 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), Publisher: ASSOC COMPUTING MACHINERY, Pages: 1259-1267

Conference paper

Ezekiel J, Lomuscio AR, 2016, Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems, Information and Computation, Vol: 254, Pages: 167-194, ISSN: 1090-2651

We present an automated technique that combines fault injection with model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems. We define a general method for mutating a multi-agent systems model representing correct behaviour by injecting faults into it, and specification patterns based on temporal-epistemic formulas to reason about the correct and faulty behaviours of the mutated model. The technique is implemented in a toolkit that can be used for injecting automatically faults into a multi-agent systems program. The usefulness of the methodology is demonstrated by injecting a number of faults into a model of the IEEE 802.5 token ring LAN protocol and analysing the protocol's fault tolerance, by verifying a number of temporal-epistemic specifications.

Journal article

Kouvaros P, Lomuscio A, 2016, Parameterised model checking for alternating-time temporal logic, 22nd European Conference on Artificial Intelligence (ECAI), Publisher: IOS Press, Pages: 1230-1238, ISSN: 0922-6389

We investigate the parameterised model checking problem for specifications expressed in alternating-time temporal logic. We introduce parameterised concurrent game structures representing infinitely many games with different number of agents. We introduce a parametric variant of ATL to express properties of the system irrespectively of the number of agents present in the system. While the parameterised model checking problem is undecidable, we define a special class of systems on which we develop a sound and complete counter abstraction technique. We illustrate the methodology here devised on the prioritised version of the train-gate-controller.

Conference paper

Lomuscio A, Vardi MY, 2016, Preface, 4th International Workshop on Strategic Reasoning, ISSN: 2075-2180

Conference paper

Boureanu I, Kouvaros P, Lomuscio A, 2016, Verifying Security Properties in Unbounded Multiagent Systems, 2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16), Publisher: ACM, Pages: 1209-1217

We study the problem of analysing the security for an unbounded number of concurrent sessions of a cryptographic protocol. Our formal model accounts for an arbitrary number of agents involved in a protocol-exchange which is subverted by a Dolev-Yao attacker. We define the parameterised model checking problem with respect to security requirements expressed in temporal-epistemic logics. We formulate sufficient conditions for solving this problem, by analysing several finite models of the system. We primarily explore authentication and key-establishment as part of a larger class of protocols and security requirements amenable to our methodology. We introduce a tool implementing the technique, and we validate it by verifying the NSPK and ASRPC protocols.

Conference paper

Kouvaros P, Lomuscio A, 2016, Formal Verification of Opinion Formation in Swarms, 2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16), Publisher: ACM, Pages: 1200-1208

We investigate the formal verification of consensus protocols in swarm systems composed of arbitrary many agents. We use templates to define the behaviour of the agents in an opinion dynamics setting and formulate their verification in terms of the associated parameterised model checking problem. We define a finite abstract model that we show to simulate swarms of any size, thereby precisely encoding any concrete instantiation of the swarm. We give an automatic procedure for verifying temporal-epistemic properties of consensus protocols by model checking the associated finite abstract model. We present a toolkit that can be used to generate the abstract model automatically and verify a given protocol by symbolic model checking. We use the toolkit to verify the correctness of majority rule protocols in arbitrary large swarms.

Conference paper

Lomuscio A, Michaliszyn J, 2016, Verification of Multi-Agent Systems via Predicate Abstraction against ATLK Specifications, 2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16), Publisher: ACM, Pages: 662-670

Conference paper

Lomuscio AR, Michaliszyn J, 2016, Model Checking Multi-Agent Systems against Epistemic HS Specifications with Regular Expressions, 15th International Conference on Principles of Knowledge Representation and Reasoning (KR16)., Publisher: Association for the Advancement of Artificial Intelligence, Pages: 298-307

We introduce EHS+, a novel temporal-epistemic logic definedon temporal intervals characterised by regular expressions.We investigate the complexity of verifying multi-agent systemsagainst EHS+specifications for a number of fragmentsof EHS+ with results ranging from PSPACE-completeness tonon-elementary time. The findings show that, at least for thefragments under analysis, the increase in expressiveness obtainedby using regular expressions rather than end-points asstandard, can be achieved without increasing the complexityof the problem. We show that the expressiveness of regularexpressions can also be adopted at the level of specificationswithout severe computational cost. To do so we introducea further temporal-epistemic logic, called EHSRE, in whichregular expressions are used within propositions, and give apolynomial time reduction of the model checking problemfrom EHSRE to EHS+.

Conference paper

Lomuscio AR, kouvaros, 2016, Parameterised verification for multi-agent systems, Artificial Intelligence, Vol: 234, Pages: 152-189, ISSN: 1872-7921

We study the problem of verifying role-based multi-agent systems, where the number of components cannot be determined at design time. We give a semantics that captures parameterised, generic multi-agent systems and identify three notable classes that represent different ways in which the agents may interact among themselves and with the environment. While the verification problem is undecidable in general we put forward cutoff procedures for the classes identified. The methodology is based on the existence of a notion of simulation between the templates for the agents and the template for the environment in the system. We show that the cutoff identification procedures as well as the general algorithms that we propose are sound; for one class we show the decidability of the verification problem and present a complete cutoff procedure. We report experimental results obtained on MCMAS-P, a novel model checker implementing the parameterised model checking methodologies here devised.

Journal article

Belardinelli F, Lomuscio A, 2016, A Three-Value Abstraction Technique for the Verification of Epistemic Properties in Multi-agent Systems, 15th European Conference on Logics in Artificial Intelligence (JELIA), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 112-126, ISSN: 0302-9743

Conference paper

Belardinelli F, Lomuscio A, Michaliszyn J, 2016, Agent-based Refinement for Predicate Abstraction of Multi-Agent Systems, Publisher: IOS Press, Pages: 286-294

Conference paper

Belardinelli F, Lomuscio A, 2016, Abstraction-based Verification of Infinite-state Reactive Modules, Publisher: IOS Press, Pages: 725-733

Conference paper

Lomuscio AR, griesmayer A, gonzalez, 2015, Verification of GSM-based Artifact-centric Systems by Predicate Abstraction, International Conference on Service-Oriented Computing, Publisher: Springer, Pages: 253-268, ISSN: 0302-9743

Artifact-centric systems are a recent paradigm to model and implementbusiness workflows. They describe data, processes, internal and external agents and include mechanisms for data hiding and access control. GSM is a language for the implementation of artifact-centric systems. Since GSM programs have infinitely many states, their verification is challenging. We here present a predicate abstraction technique that enables us to verify GSM programs against richspecifications built on an epistemic, first-order variant of the µ-calculus. We give the theoretical underpinnings of the technique and presentGSMC, the first model checker for GSM that implements SMT-based, three-valued abstraction for GSM.

Conference paper

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.

Journal article

Lomuscio AR, Kouvaros P, Verifying Emergent Properties of Swarms, Twenty-Fourth International Conference on Artificial Intelligence (IJCAI15), Publisher: AAAI Press, Pages: 1083-1089

Conference paper

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

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=1&respub-action=search.html