Publications
232 results found
Lomuscio A, Strulo B, Walker N, et al., 2010, Assume-Guarantee Reasoning with Local Specifications, 12th International Conference on Formal Engineering Methods, Publisher: SPRINGER-VERLAG BERLIN, Pages: 204-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 10
Belardinelli F, Lomuscio A, 2010, First-Order Linear-time Epistemic Logic Group Knowledge: An Axiomatisation of the Monodic Fragment, Fundamenta Informaticae, Vol: 106, Pages: 175-190
Lomuscio A, Solanki M, Penczek W, et al., 2010, Runtime monitoring of contract regulated web services., Publisher: IFAAMAS, Pages: 1449-1450
Belardinelli F, Lomuscio A, 2010, Interactions between knowledge and time in a first-order logic for multi-agent systems, Publisher: AAAI Press, Pages: 38-48
Lomuscio A, Walker NG, Strulo B, et al., 2010, Model Checking Optimisation Based Congestion Control Algorithms, Publisher: IOS PRESS, Pages: 77-96, ISSN: 0169-2968
- Author Web Link
- Cite
- Citations: 1
Kwiatkowska M, Lomuscio A, Qu H, 2010, Parallel Model Checking for Temporal Epistemic Logic, 19th European Conference on Artificial Intelligence (ECAI)/6th Conference on Prestigious Applications of Intelligent Systems (PAIS), Publisher: IOS PRESS, Pages: 543-548, ISSN: 0922-6389
- Author Web Link
- Cite
- Citations: 10
Cohen M, Lomuscio A, 2010, Non-elementary speed up for model checking synchronous perfect recall, 19th European Conference on Artificial Intelligence (ECAI)/6th Conference on Prestigious Applications of Intelligent Systems (PAIS), Publisher: IOS PRESS, Pages: 1077-+, ISSN: 0922-6389
- Author Web Link
- Cite
- Citations: 2
Lomuscio A, Penczek W, Qu H, 2010, Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems, FUNDAMENTA INFORMATICAE, Vol: 101, Pages: 71-90, ISSN: 0169-2968
- Author Web Link
- Cite
- Citations: 19
Cohen M, Dam M, Russo F, et al., 2009, Abstraction in model checking multi-agent systems, Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, Vol: 1, Pages: 710-717, ISSN: 1548-8403
We present an abstraction technique for multi-agent, systems preserving temporal-epistcrnic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain. Copyright © 2009, International Foundation for Autonomous Agents and Multiagent Systems.
Cohen M, Dam M, Lomuscio A, et al., 2009, A symmetry reduction technique for model checking temporal-epistemic logic, Departmental Technical Report: 09/1, Publisher: Department of Computing, Imperial College London, 09/1
We introduce a symmetry reduction technique for model checking temporalepistemicproperties of multi-agent systems defined in the mainstream interpretedsystems framework. The technique, based on counterpart semantics, aims to reducethe set of initial states that need to be considered in a model. We presenttheoretical results establishing that there are neither false positives nor false negativesin the reduced model. We evaluate the technique by presenting the results ofan implementation tested against two well known applications of epistemic logic,the muddy children and the dining cryptographers. The experimental results obtainedconfirm that the reduction in model checking time can be dramatic, therebyallowing for the verification of hitherto intractable systems.
Lomuscio A, Ezekiel J, 2009, Combining fault injection and model checking to verify fault tolerance in multi-agent systems, Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, Vol: 1, Pages: 86-93, ISSN: 1548-8403
The ability to guarantee that a system will continue to operate correctly under degraded conditions is key to the success of adopting multi-agent systems (MAS) as a paradigm for designing complex agent based fault tolerant systems. In order to provide such a guarantee, practically usable tools and techniques for verifying fault tolerant MAS architectures are urgently required. In this paper we address this requirement by combining automatic fault injection with model check-ing to verify fault tolerance in MAS. We present a generic method to mutate a model of a correctly behaving system into a faulty one, and show how the mutated model can be used to reason about fault tolerance, which includes recovery from faults. The usefulness of the proposed method is demonstrated by injecting automatically a fault into a sender-receiver protocol, and verifying temporal and epis- Temic specifications of the protocol's fault tolerance using the MCMAS model checker. Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Model Check-ing General Terms Verification. Copyright © 2009, International Foundation for Autonomous Agents and Multiagent Systems.
Boureanu I, Cohen M, Lomuscio A, 2009, Automatic verification of temporal-epistemic properties of cryptographic protocols., Journal of Applied Non-Classical Logics, Vol: 19, Pages: 463-487, ISSN: 1166-3081
Lomuscio A, Solanki M, 2009, Mapping OWL-S processes to multi agent systems: a verification oriented approach, 23rd International Conference on Advanced Information Networking and Applications Workshops, Publisher: IEEE, Pages: 488-493
- Author Web Link
- Cite
- Citations: 3
Lomuscio A, Solanki M, 2009, Towards an Agent Based Approach for Verification of OWL-S Process Models, 6th European Sematic Web Conference, Publisher: SPRINGER-VERLAG BERLIN, Pages: 578-592, ISSN: 0302-9743
Lomuscio A, Qu H, Raimondi F, 2009, MCMAS: A model checker for Multiagent systems, London
Belardinelli F, Lomuscio A, 2009, First-Order Linear-Time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment, Publisher: Springer, Pages: 140-154
Belardinelli F, Lomuscio A, 2009, Quantified Epistemic Logics for Reasoning About Knowledge in Multi-Agent Systems, Artificial Intelligence, Vol: 173, Pages: 982-1013
Lomuscio A, Penczek W, Qu H, 2009, Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic, 5th International Workshop on Model Checking and Artificial Intelligence (MoChArt 2008), Publisher: SPRINGER-VERLAG BERLIN, Pages: 106-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 1
Lomuscio A, Qu H, Raimondi F, 2009, MCMAS: A Model Checker for the Verification of Multi-Agent Systems, 21st International Conference on Computer Aided Verification, Publisher: SPRINGER-VERLAG BERLIN, Pages: 682-688, ISSN: 0302-9743
Cohen M, Dam M, Lomuscio A, et al., 2009, A Data Symmetry Reduction Technique for Temporal-epistemic Logic, 7th International Symposium on Automated Technology for Verification and Analysis, Publisher: SPRINGER-VERLAG BERLIN, Pages: 69-83, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 5
Cohen M, Dam M, Lomuscio A, et al., 2009, Abstraction in model checking multi-agent systems., Publisher: IFAAMAS, Pages: 945-952
Cohen M, Dam M, Lomuscio A, et al., 2009, A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic, 21st International Joint Conference on Artificial Intelligence (IJCAI-09), Publisher: IJCAI-INT JOINT CONF ARTIF INTELL, Pages: 721-726
- Author Web Link
- Cite
- Citations: 16
Ezekiel J, Lomuscio A, 2009, An automated approach to verifying diagnosability in multi-agent systems, 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009), Publisher: IEEE COMPUTER SOC, Pages: 51-60
- Author Web Link
- Cite
- Citations: 3
Ezekiel J, Lomuscio A, 2009, Combining fault injection and model checking to verify fault tolerance in multi-agent systems., Publisher: IFAAMAS, Pages: 113-120
Lomuscio A, Qu H, Solanki M, 2008, Towards verifying contract regulated service composition, Pages: 254-261
We report on a novel approach to (semi-)automatically compile and verify contract-regulated service compositions. We specify web services and the contracts governing them as WSBPEL behaviours. We compile WSBPEL behaviours into the specialised system description language ISPL, to be used with the model checker MCMAS to verify behaviours automatically. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivating example whose state space is approximately 106 and discuss experimental results. © 2008 IEEE.
Belardinelli F, Lomuscio A, 2008, A complete first-order logic of knowledge and time, Pages: 705-714, ISSN: 2334-1025
We introduce and investigate quantified interpreted systems, a semantics to reason about knowledge and time in a firstorder setting. We provide an axiomatisation, which we show to be sound and complete. We utilise the formalism to study message passing systems (Lamport 1978; Fagin et al 1995) in a first-order setting, and compare the results obtained to those available for the propositional case. Copyright © 2008, Association for the Advancement of Artificial Intelligence.
Lomuscio A, Qu H, Solanki M, 2008, Towards verifying compliance in agent-based Web service compositions, Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, Vol: 1, Pages: 262-269, ISSN: 1548-8403
We explore the problem of specification and verification of compliance in agent based Web service compositions. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivating example where the behaviours of participating agents are governed by contracts. The composition is specified in OWL-S and mapped to our chosen formalism. Finally we use an existing symbolic model checker to verify the example specification whose state space is approximately 221 and discuss experimental results. Copyright © 2008, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
Belardinelli F, Lomuscio A, 2008, A Complete Quantified Epistemic Logic for Reasoning about Message Passing Systems, 8th International Workshop on Computational Logic in Multi-Agent Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 248-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 1
Lomuscio A, Penczek W, 2008, LDYIS: a Framework for Model Checking Security Protocols, Concurrency Specification and Programming Workshop, Publisher: IOS PRESS, Pages: 359-375, ISSN: 0169-2968
- Author Web Link
- Cite
- Citations: 7
Lomuscio A, Qu H, Solanki M, 2008, Towards verifying compliance in agent-based web service compositions., Publisher: IFAAMAS, Pages: 265-272
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.