176 results found
Lomuscio AR, Vardi MY, 2018, 4th International Workshop on Strategic Reasoning (SR 2016), Information and Computation, Vol: 261, ISSN: 0890-5401
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
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, 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 INT PUBLISHING AG, Pages: 112-126, ISSN: 0302-9743
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
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.
Kouvaros P, Lomuscio A, 2016, Parameterised verification for multi-agent systems, ARTIFICIAL INTELLIGENCE, Vol: 234, Pages: 152-189, ISSN: 0004-3702
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.
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
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 MCMAS PA , a toolkit implementing the technique here described. MCMAS PA 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 MCMAS PA can verify infinite-state multi-agent systems of interest.
Lomuscio A, Vardi MY, 2016, Preface, ISSN: 2075-2180
Belardinelli F, Grossi D, Lomuscio A, 2015, Finite abstractions for the verification of epistemic properties in open multi-agent systems, Pages: 854-860, ISSN: 1045-0823
We develop a methodology to model and verify open multi-agent systems (OMAS), where agents may join in or leave at run time. Further, we specify properties of interest on OMAS in a variant of firstorder temporal-epistemic logic, whose characterising features include epistemic modalities indexed to individual terms, interpreted on agents appearing at a given state. This formalism notably allows to express group knowledge dynamically. We study the verification problem of these systems and show that, under specific conditions, finite bisimilar abstractions can be obtained.
Gonzalez P, Griesmayer A, Lomuscio A, 2015, Verification of GSM-Based Artifact-Centric Systems by Predicate Abstraction, 13th 1nternational Conference on Service-Oriented Computing (ICSOC), Publisher: SPRINGER INT PUBLISHING AG, Pages: 253-268, ISSN: 0302-9743
Grandi F, Lange M, Lomuscio A, 2015, Message from Programme Co-chairs
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.
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.
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.
Lomuscio A, Michaliszyn J, 2015, Verifying multi-agent systems by model checking three-valued abstractions, Pages: 189-198, ISSN: 1548-8403
Copyright © 2015, International Foundation for Autonomous Agents and Multiagent Systems. We develop the theoretical foundations of a predicate abstraction methodology for the verification of multi-agent systems. We put forward a specification language based on epistemic logic and a weak variant of the logic ATL interpreted on a three-valued semantics. We show that the model checking problem for multi-agent systems in this setting is tractable by giving a provably correct procedure which admits a PTIME bound. We give a constructive technique for generating abstract approximations of concrete multi-agent systems models and show that the truth values are preserved between abstract and concrete models. We evaluate the effectiveness of the methodology on a variant of the bit-transmission problem.
Lomuscio A, Michaliszyn J, 2015, Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions., CoRR, Vol: abs/1509.00608
Lomuscio A, Paquet H, 2015, Verification of multi-agent systems via SDD-based model checking, Pages: 1713-1714, ISSN: 1548-8403
Copyright © 2015, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved. Considerable progress has been achieved in the past ten years in the symbolic verification of Multi-Agent Systems (MAS). One of the most efficient techniques put forward is based on the use of ordered binary decision diagrams (OBDDs) for representing the state space and computing the states at which specifications hold. Sentential Decision Diagrams (SDDs) have recently been put forward as an alternative symbolic representation for Boolean formulas in knowledge representation. In this abstract we report some preliminary results on the applicability of SDDs for the verification of MAS.
Lomuscio AR, Qu H, Raimondi F, 2015, 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.
Č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.
, 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, JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, Vol: 51, Pages: 333-376, ISSN: 1076-9757
Belardinelli F, Lomuscio A, Patrizi F, 2014, Verification of Agent-Based Artifact Systems., J. Artif. Intell. Res., Vol: 51, Pages: 333-376
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 A, Michaliszyn J, 2014, Model checking unbounded artifact-centric systems, Pages: 488-497
Copyright © 2014, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. Artifact-centric systems are a recent paradigm for representing and implementing business processes. We present further results on the verification problem of artifact-centric systems specified by means of FO-CTL specifications. While the general problem is known to be undecidable, results in the literature prove decidability for artifact systems with infinite domains under boundedness and conditions such as uniformity. We here follow a different approach and investigate the general case with infinite domains. We show decidability of the model checking problem for the class of artifact-centric systems whose database schemas consist of a single unary relation, and we show that that the problem is undecidable if artifact systems are defined by using one binary relation or two unary relations.
Lomuscio A, Michaliszyn J, 2014, An abstraction technique for the verification of multi-agent systems against ATL specifications, Pages: 428-437
Copyright © 2014, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. We introduce an abstraction methodology for the verification of multi-agent systems against specifications expressed in alternating-time temporal logic (ATL). Inspired by methodologies such as predicate abstraction, we define a three-valued semantics for the interpretation of ATL formulas on concurrent game structures and compare it to the standard two-valued semantics. We define abstract models and establish preservation results on the three-valued semantics between abstract models and their concrete counterparts. We illustrate the methodology on the large state spaces resulting from a card game.
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.