181 results found
Lomuscio A, Michaliszyn J, 2015, Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions., CoRR, Vol: abs/1509.00608
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
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
Čermák 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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 8559 LNCS, 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, 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
, 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.
, 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.
Belardinelli F, Lomuscio A, Patrizi F, 2014, Verification of Agent-Based Artifact Systems., J. Artif. Intell. Res., Vol: 51, Pages: 333-376
, 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
Lomuscio A, Moss LS, Ovchinnikova E, et al., 2014, Tutorials., Publisher: AAAI Press
, 2013, A cutoff technique for the verification of parameterised interpreted systems with parameterised environments, 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.
, 2013, Decidability of model checking non-uniform artifact-centric quantified interpreted systems, Pages: 725-731, ISSN: 1045-0823
Artifact-Centric Systems are a novel paradigm in service-oriented computing. In the present contribution we show that model checking bounded, nonuniform artifact-centric systems is undecidable. We provide a partial model checking procedure for artifact-centric systems against the universal fragment of a first-order version of the logic CTL. We obtain this result by introducing a counterpart semantics and developing an abstraction methodology operating on these structures. This enables us to generate finite abstractions of infinite artifact-centric systems, hence perform verification on abstract models.
, 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.
, 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
, 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.
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
, 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.
, 2012, An abstraction technique for the verification of artifact-centric systems, Pages: 319-328
We explore the paradigm of artifact-centric systems from a knowledge-based perspective. We provide a semantics based on interpreted-systems to interpret a first-order temporal-epistemic language with identity in a multi-agent setting. We consider the model checking problem for this language and provide abstraction results. We isolate a natural subclass of artifact-systems for which the model checking problem is de-cidable. We give an upper bound on the complexity of the model checking problem. Copyright © 2012, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
, 2012, Verification of GSM-based artifact-centric systems through finite abstraction, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 7636 LNCS, Pages: 17-31, ISSN: 0302-9743
The GSM framework provides a methodology for the development of artifact-centric systems, an increasingly popular paradigm in service-oriented computing. In this paper we tackle the problem of verifying GSM programs in a multi-agent system setting. We provide an embedding from GSM into a suitable multi-agent systems semantics for reasoning about knowledge and time at the first-order level. While we observe that GSM programs generate infinite models, we isolate a large class of "amenable" systems, which we show admit finite abstractions and are therefore verifiable through model checking. We illustrate the contribution with a procurement use-case taken from the relevant business process literature. © Springer-Verlag Berlin Heidelberg 2012.
, 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, Pages: 48-62
, 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.
, 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.
Lomuscio A, Qu H, Solanki M, 2012, Towards verifying contract regulated service composition, AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS, Vol: 24, Pages: 345-373, ISSN: 1387-2532
Belardinelli F, Lomuscio A, 2012, Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results, JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, Vol: 45, Pages: 1-45, ISSN: 1076-9757
Jones AV, Knapik M, Lomuscio A, et al., 2012, Group synthesis for parametric temporal-epistemic logic, 11th International Conference on Autonomous Agents and Multiagent Systems 2012, AAMAS 2012: Innovative Applications Track, Vol: 2, Pages: 880-887
We investigate parameter synthesis in the context of temporal-epistemic logic. We introduce CTLPK, a parametric extension to the branching time temporal-epistemic logic CTLK with free variables representing groups of agents. We give algorithms for automatically synthesising the groups of agents that make a given parametric formula satisfied. We discuss an implementation of the technique on top of the open-source model checker MCMAS and demonstrate its attractiveness by reporting the experimental results obtained. Copyright © 2012, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
, 2012, Automatic verification of epistemic specifications under convergent equational theories, 11th International Conference on Autonomous Agents and Multiagent Systems 2012, AAMAS 2012: Innovative Applications Track, Vol: 2, Pages: 1072-1079
We present a methodology for the automatic verification of multi-agent systems against temporal-epistemic specifications derived from higher-level languages defined over convergent equational theories. We introduce a modality called rewriting knowledge that operates on local equalities. We discuss the conditions under which its interpretation can be approximated by a second modality that we introduce called empirical knowledge. Empirical knowledge is computationally attractive from a verification perspective. We report on an implementation of a technique to verify this modality with the open source model checker MCMAS. We evaluate the approach by verifying multi-agent models of electronic voting protocols automatically extracted from high-level descriptions. Copyright © 2012, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
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.