Publications
232 results found
Jones AV, Knapik M, Lomuscio A, et al., 2013, Group synthesis for alternating-time temporal logic, Departmental Technical Report: 13/9, Publisher: Department of Computing, Imperial College London, 13/9
We present an extension of Alternating-time Temporal LogicATL, called ATLP (Parametric ATL), where parameters are allowed inplace of concrete groups of agents. We devise a procedure to nd all instantiationsfor the parameters in a given formula of ATLP so that is true in a given model. We propose a formalisation of the problemand symbolic algorithms for its solution. We discuss an experimental implementationof the approach on top of the open-source model checkermcmas and demonstrate the bene ts of the technique through experimentalresults.
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
Kouvaros P, Lomuscio A, 2013, Automatic verification of parameterised multi-agent systems., Publisher: IFAAMAS, Pages: 861-868
Belardinelli F, Lomuscio A, 2013, Decidability of Model Checking Non-Uniform Artifact-Centric Quantified Interpreted Systems, Publisher: AAAI Press, Pages: 725-731
Griesmayer A, Lomuscio A, 2013, Model Checking Distributed Systems against Temporal-Epistemic Specifications, Joint IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems (33rd FMOODS/15th FORTE) Held as Part of the 8th International Federated Conference on Distributed Computing Techniques (DisCoTec), Publisher: SPRINGER-VERLAG BERLIN, Pages: 130-145, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 2
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.
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.
Barker S, Jones AJI, Kakas A, et 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.
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.
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
- Author Web Link
- Open Access Link
- Cite
- Citations: 25
Boureanu I, Jones AV, Lomuscio A, 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.
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.
De Giacomo G, Felli P, Lomuscio A, 2012, Synthesizing agent protocols from LTL specifications against multiple partially-observable environments, Pages: 457-466, ISSN: 2334-1025
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.
Belardinelli F, Lomuscio A, Patrizi F, 2012, Verification of GSM-based artifact-centric systems through finite abstraction, Proceedings of the 10th International Conference on Service Oriented Computing (ISCOC12), Vol: 7636, Pages: 17-31
Belardinelli F, Lomuscio A, Patrizi F, 2012, Verification of GSM-Based Artifact-Centric Systems through Finite Abstraction, Publisher: Springer, Pages: 17-31
Jones AV, Knapik M, Penczek W, et al., 2012, Group synthesis for parametric temporal-epistemic logic., Publisher: IFAAMAS, Pages: 1107-1114
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
Belardinelli F, Lomuscio A, Patrizi F, 2012, An Abstraction Technique for the Verification of Artifact-Centric Systems, Publisher: AAAI Press, Pages: 319-328
Boureanu I, Jones AV, Lomuscio A, 2012, Automatic verification of epistemic specifications under convergent equational theories., Publisher: IFAAMAS, Pages: 1141-1148
Ezekiel J, Lomuscio A, Molnar L, et al., 2011, Verifying fault tolerance and self-diagnosability of an autonomous underwater vehicle, Pages: 1659-1664, ISSN: 1045-0823
We report the results obtained during the verification of Autosub6000, an autonomous underwater vehicle used for deep oceanic exploration. Our starting point is the Simulink/Matlab engineering model of the submarine, which is discretised by a compiler into a representation suitable for model checking. We assess the ability of the vehicle to function under degraded conditions by injecting faults automatically into the discretised model. The resulting system is analysed by means of the model checker MCMAS, and conclusions are drawn on the system's ability to withstand faults and to perform self-diagnosis and recovery. We present lessons learnt from this and suggest a general method for verifying autonomous vehicles.
Lomuscio A, Qu H, Russo F, 2011, Automatic data-abstraction in model checking multi-agent systems, Pages: 52-68, ISSN: 0302-9743
We present an automatic data-abstraction technique for the verification of the universal fragment of the temporal-epistemic logic CTLK. We show the correctness of the methodology and present an implementation operating on ISPL models, the input files for MCMAS, a model checker for multi-agent systems. The experimental results point to the attractiveness of the technique in a number of examples in the multi-agent systems domain. © 2011 Springer-Verlag.
Belardinelli F, Lomuscio A, Patrizi F, 2011, A computationally grounded semantics for artifact centric systems and abstraction results, Publisher: AAAI Press, Pages: 738-743
Belardinelli F, Lomuscio A, Patrizi F, 2011, Verification of deployed artifact systems via data abstraction, Publisher: Springer, Pages: 142-156
Belardinelli F, Jones AV, Lomuscio A, 2011, Model Checking Temporal-Epistemic Logic Using Alternating Tree Automata, Fundamenta Informaticae, Vol: 112, Pages: 19-37
Lomuscio A, Penczek W, Solanki M, et al., 2011, Runtime Monitoring of Contract Regulated Web Services, FUNDAMENTA INFORMATICAE, Vol: 111, Pages: 339-355, ISSN: 0169-2968
- Author Web Link
- Cite
- Citations: 5
Cohen M, Lomuscio A, 2010, Non-elementary speed up for model checking synchronous perfect recall, Departmental Technical Report: 10/9, Publisher: Department of Computing, Imperial College London, 10/9
We analyse the time complexity of the model checkingproblem for a logic of knowledge and past time in synchronoussystems with perfect recall. Previously established bounds are k-exponential in the size of the system for specifications with k nestedknowledge modalities.We show that the upper bound for positive (respectively,negative) specifications is polynomial (respectively, exponential)in the size of the system irrespective of the nesting depth.
Lomuscio A, Penczek W, Qu H, 2010, Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems, Pages: 659-666, ISSN: 1548-8403
We investigate partial order reduction Tor model checking multi-agent systems by focusing on interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed. We present a notion of stuttering-equivalence, and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model checking step and show preservation properties. We evaluate the technique by discussing the experimental results obtained against well-known examples in the MAS literature. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
Jones AV, Lomuscio A, 2010, Distributed BDD-based BMC for the verification of multi-agent systems, Pages: 675-682, ISSN: 1548-8403
We present a method of distributed model checking of multi-agent systems specified by a branching-time temporal-epistemic logic. We introduce a serial algorithm, central to the distributed approach, for combining binary decision diagrams with bounded model checking. The algorithm is based on a notion of "seed states" to allow for state-space partitioning. Exploring individual partitions displays benefits arising from the verification of partial state-spaces. When verifying both an industrial model and a scalable benchmark scenario the serial bounded technique was found to be effective. Results for the distributed technique demonstrate that it out-performs the sequential approach for falsifiable formulae. Experimental data indicates that increasing the number of hosts improves verification efficiency. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
Boureanu I, Cohen M, Lomuscio A, 2010, Model checking detectability of attacks in multiagent systems, Pages: 691-698, ISSN: 1548-8403
Information security is vital to many multiagent system applications. In this paper we formalise the notion of detectability of attacks in a MAS setting and analyse its applicability. We introduce a taxonomy of detectability specifications expressed in temporal-epistemic logic. We illustrate the practical relevance of attack detectability in a case study applied to a variant of Kerberos protocol. We model-check attack detectability in automatically generated MAS models for security protocols. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
Ezekiel J, Lomuscio A, 2010, A Methodology for Automatic Diagnosability Analysis, 12th International Conference on Formal Engineering Methods, Publisher: SPRINGER-VERLAG BERLIN, Pages: 549-564, ISSN: 0302-9743
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.