181 results found
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
Boureanu I, Jones AV, Lomuscio A, 2012, Automatic verification of epistemic specifications under convergent equational theories., Publisher: IFAAMAS, Pages: 1141-1148
, 2011, A computationally-grounded semantics for artifact-centric systems and abstraction results, Pages: 738-743, ISSN: 1045-0823
We present a formal investigation of artifact-based systems, a relatively novel framework in service oriented computing, aimed at laying the foundations for verifying these systems through model checking. We present an infinite-state, computationally grounded semantics for these systems that allows us to reason about temporal-epistemic specifications. We present abstraction techniques for the semantics that guarantee transfer of satisfaction from the abstract system to the concrete one.
, 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.
, 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, Verification of Deployed Artifact Systems via Data Abstraction, 9th International Conference on Service-Oriented Computing (ICSOC), Publisher: SPRINGER-VERLAG BERLIN, Pages: 142-156, ISSN: 0302-9743
Belardinelli F, Jones AV, Lomuscio A, 2011, Model Checking Temporal-Epistemic Logic Using Alternating Tree Automata, FUNDAMENTA INFORMATICAE, Vol: 112, Pages: 19-37, ISSN: 0169-2968
Belardinelli F, Lomuscio A, 2011, First-Order Linear-time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment, FUNDAMENTA INFORMATICAE, Vol: 106, Pages: 175-190, ISSN: 0169-2968
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
, 2010, Interactions between time and knowledge in a first-order logic for multi-agent systems, Pages: 38-48
We investigate a class of first-order temporal epistemic logics for the specification of multi-agent systems. We consider well-known properties of multi-agent systems including perfect recall, synchronicity, no learning, unique initial state, and define natural correspondences between these and quantified interpreted systems. Our findings identify several monodic fragments of first-order temporal epistemic logic that we prove to be both sound and complete with respect to the corresponding classes of quantified interpreted systems. The results show that interaction axioms for propositional temporal epistemic logic can be lifted to the monodic fragment. Copyright © 2010, Association for the Advancement of Artificial Intelligence.
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
, 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.
, 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.
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
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
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.
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
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
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
Lomuscio A, Solanki M, Penczek W, et al., 2010, Runtime monitoring of contract regulated web services., Publisher: IFAAMAS, Pages: 1449-1450
, 2009, Automatic verification of temporal-epistemic properties of cryptographic protocols, Journal of Applied Non-Classical Logics, Vol: 19, Pages: 463-487, ISSN: 1166-3081
We present a technique for automatically verifying cryptographic protocols specified in the mainstream specification language CAPSL. We define a translation from CAPSL models into interpreted systems, a popular semantics for temporal-epistemic logic, and rewrite CAPSL goals as temporal-epistemic specifications. We present a compiler that implements this translation. The compiler links to the symbolic model checker MCMAS. We evaluate the technique on protocols in the Clark-Jacobs library and in the SPORE repository against custom secrecy and authentication requirements.
Belardinelli F, Lomuscio A, 2009, Quantified epistemic logics for reasoning about knowledge in multi-agent systems, ARTIFICIAL INTELLIGENCE, Vol: 173, Pages: 982-1013, ISSN: 0004-3702
Belardinelli F, Lomuscio A, 2009, First-Order Linear-Time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment, 16th International Workshop on Logic, Language, Information and Computation, Publisher: SPRINGER-VERLAG BERLIN, Pages: 140-154, ISSN: 0302-9743
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
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-+, ISSN: 0302-9743
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.
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
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
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
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.