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.
Fu H, Ghosh A, Kopf J, 2018, Preface, Publisher: WILEY, ISSN: 0167-7055
Lomuscio AR, Vardi MY, 2018, 4th International Workshop on Strategic Reasoning (SR 2016) Preface, Publisher: ACADEMIC PRESS INC ELSEVIER SCIENCE, Pages: 615-615, ISSN: 0890-5401
Čermák P, Lomuscio A, Mogavero F, et al., 2018, Practical verification of multi-agent systems against Slk specifications, Information and Computation, Vol: 261, Pages: 588-614, ISSN: 0890-5401
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.
Lomuscio AR, akitunde M, maganti L, et 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.
Belardinelli F, Lomuscio A, Malvone V, Approximating Perfect Recall when Model Checking Strategic Abilities, Knowledge Representation and Reasoning
Belardinelli F, Murano A, Lomuscio A, et al., 2018, Decidable verification of multi-agent systems with bounded private actions, Pages: 1865-1867, ISSN: 1548-8403
Belardinelli F, Lomuscio A, Murano A, et al., 2018, Alternating-time temporal logic on finite traces, 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.
Ezekiel J, Lomuscio A, 2017, 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: 0890-5401
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.
Belardinelli F, Lomuscio A, Murano A, et al., 2017, Verification of broadcasting multi-agent systems against an epistemic strategy logic, Pages: 91-97, ISSN: 1045-0823
We study a class of synchronous, perfect-recall multi-agent systems with imperfect information and broadcasting, i.e., fully observable actions. We define an epistemic extension of strategy logic with incomplete information and the assumption of uniform and coherent strategies. In this setting, we prove that the model checking problem, and thus rational synthesis, is non-elementary decidable. We exemplify the applicability of the framework on a rational secret-sharing scenario.
Belardinelli F, Lomuscio A, 2017, 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
Belardinelli F, Kouvaros P, Lomuscio A, 2017, Parameterised verification of data-aware multi-agent systems, 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.
Hasani RM, Haerle D, Baumgartner CF, et al., 2017, Compositional Neural-Network Modeling of Complex Analog Circuits, International Joint Conference on Neural Networks (IJCNN), Publisher: IEEE, Pages: 2235-2242, ISSN: 2161-4393
Belardinelli F, Lomuscio A, Murano A, et al., 2017, Verification of Multi-agent Systems with Imperfect Information and Public Actions, 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), Publisher: ASSOC COMPUTING MACHINERY, Pages: 1268-1276
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.
Lomuscio A, Vardi MY, 2016, Preface, ISSN: 2075-2180
Kouvaros P, Lomuscio A, 2016, Parameterised verification for multi-agent systems, ARTIFICIAL INTELLIGENCE, Vol: 234, Pages: 152-189, ISSN: 0004-3702
Belardinelli F, Lomuscio A, 2016, Abstraction-Based Verification of Infinite-State Reactive Modules, 22nd European Conference on Artificial Intelligence (ECAI), Publisher: IOS PRESS, Pages: 725-733, ISSN: 0922-6389
Belardinelli F, Lomuscio A, Michaliszyn J, 2016, Agent-Based Refinement for Predicate Abstraction of Multi-Agent Systems, 22nd European Conference on Artificial Intelligence (ECAI), Publisher: IOS PRESS, Pages: 286-294, ISSN: 0922-6389
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
Kouvaros P, Lomuscio A, 2016, Formal verification of opinion formation in swarms, Pages: 1200-1208, ISSN: 1548-8403
Copyright © 2016, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved. 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.
Boureanu I, Kouvaros P, Lomuscio A, 2016, Verifying security properties in unbounded multiagent systems, Pages: 1209-1217, ISSN: 1548-8403
Copyright © 2016, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved. 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.
Lomuscio A, Michaliszyn J, 2016, Model checking multi-agent systems against epistemic HS specifications with regular expressions, Pages: 298-307
Copyright © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. We introduce EHS+, a novel temporal-epistemic logic defined on temporal intervals characterised by regular expressions. We investigate the complexity of verifying multi-agent systems against EHS+ specifications for a number of fragments of EHS+ with results ranging from PSPACE-completeness to non-elementary time. The findings show that, at least for the fragments under analysis, the increase in expressiveness obtained by using regular expressions rather than end-points as standard, can be achieved without increasing the complexity of the problem. We show that the expressiveness of regular expressions can also be adopted at the level of specifications without severe computational cost. To do so we introduce a further temporal-epistemic logic, called EHSRE, in which regular expressions are used within propositions, and give a polynomial time reduction of the model checking problem from EHSRE to EHS+.
Lomuscio A, Michliszyn J, 2016, Verification of multi-agent systems via predicate abstraction against ATLK specifications, Pages: 662-670, ISSN: 1548-8403
Copyright © 2016, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved. We present a predicate abstraction technique for the verification of multi-agent systems against specifications defined in the epistemic logic ATLK, interpreted on a three-valued semantics. We reduce an infinite-state multi-agent program to a finite model by generating predicates automatically via SMT calls. We show that if an ATLK specification is either true or false in the abstract model, then that is also the case on the original infinite state model. We introduce and describe MCMASPA, a toolkit implementing the technique here described. MCMASPA supports the three-valued semantics for ATLK, automatically generates program abstractions for a multi-agent system by means of automatic SMT calls, encodes the corresponding program in BDDs and reports the result. The experimental results obtained confirm that MCMASPA can verify infinite-state multi-agent systems of interest.
Čermák P, Lomuscio A, Murano A, 2015, Verifying and synthesising multi-agent systems against one-goal strategy logic specifications, Pages: 2038-2044
© Copyright 2015, Association for the Advancement of Artificial Intelligence (www.aaa1.org). All rights reserved. Strategy Logic (SL) has recently come to the fore as a useful specification language to reason about multi-agent systems. Its one-goal fragment, or SL[1g], is of particular interest as it strictly subsumes widely used logics such as ATL∗, while maintaining attractive complexity features. In this paper we put forward an automata-based methodology for verifying and synthesising multi-agent systems against specifications given in SL[Ig], We show that the algorithm is sound and optimal from a computational point of view. A key feature of the approach is that all data structures and operations on them can be performed on BDDs. We report on a BDD-based model checker implementing the algorithm and evaluate its performance on the fair process scheduler synthesis.
Kouvaros P, Lomuscio A, 2015, A counter abstraction technique for the verification of robot swarms, Pages: 2081-2088
© Copyright 2015, Association for the Advancement of Artificial Intelligence (www.aaa1.org). All rights reserved. We study parameterised verification of robot swarms against temporal-epistemic specifications. We relax some of the significant restrictions assumed in the literature and present a counter abstraction approach that enable us to verify a potentially much smaller abstract model when checking a formula on a swarm of any size. We present an implementation and discuss experimental results obtained for the alpha algorithm for robot swarms.
Grandi F, Lange M, Lomuscio A, 2015, Message from Programme Co-chairs
Kouvaros P, Lomuscio A, 2015, Verifying emergent properties of swarms, Pages: 1083-1089, ISSN: 1045-0823
We investigate the general problem of establishing whether a swarm satisfies an emergent property. We put forward a formal model for swarms that accounts for their nature of unbounded collections of agents following simple local protocols. We formally define the decision problem of determining whether a swarm satisfies an emergent property. We introduce a sound and complete procedure for solving the problem. We illustrate the technique by applying it to the Beta aggregation algorithm.
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.