1,721,088 research outputs found
Synthesizing agent protocols from LTL specifications against multiple partially-observable environments
No full textWe 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
A computationally-grounded semantics for artifact-centric systems and abstraction results
No full textWe 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
Complexity of ITL model checking: some well-behaved fragments of the interval logic HS
No full textModel checking has been successfully used in many computer science fields, including artificial intelligence, theoretical computer science, and databases. Most of the proposed solutions make use of classical, point-based temporal logics, while little work has been done in the interval temporal logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham’s modal logic of time intervals HS over finite Kripke structures (under the homogeneity assumption) and an EXPSPACE model checking procedure for two meaningful fragments of it have been proposed. In this paper, we show that more efficient model checking procedures can be developed for some expressive enough fragments of HS
MCMAS-SL[1G]: A model checker for the verification of one-goal strategy logic specifications
No full textModel 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 wor
Verification of GSM-based artifact-centric systems through finite abstraction
Full text linkThe 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
Verification of deployed artifact systems via data abstraction
No full textArtifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycle models, accounting for the relational structure of the artifact state and its possible evolutions over time. We consider the problem of verifying artifact systems against specifications expressed in quantified temporal logic. This problem is in general undecidable. However, when artifact systems are deployed, their states can contain only a bounded number of elements. We exploit this fact to develop an abstraction technique that enables us to verify deployed artifact systems by model checking their bounded abstraction
Message from Programme Co-chairs
No full textThe 22nd International Symposium on Temporal Representation and Reasoning (TIME 2015) was held
in Kassel, Germany, between the 23rd and the 25th of September 2015.
The TIME Symposium series aims to bring together researchers interested in reasoning about temporal
aspects of information in any area of Computer Science. The symposium series has a wide remit and
intends to cater both for theoretical aspects and well-founded applications. One of the key aspects of the
TIME symposium is its interdisciplinarity with attendees from distinct areas such as artificial intelligence,
database management, logic and verification, and beyond
Temporal Aspects of Big Data Management: State-of-the-Art Analysis and Future Research Directions
No full textA great deal of research efforts has been invested in temporal aspects of big data management during last years, with alternate fortune. This line of research aims at capturing, formally modeling and successfully exploiting all the time-dependent characteristics of the fundamental big data model ranging from state model to query model. Temporal big data management thus poses novel research challenges and exciting directions to be followed, and a first critical result is represented by recognizing that traditional time-focused models, techniques and algorithms developed in previous years are not suitable to deal with novel characteristics of big data, mainly due to volume, heterogeneity and scalability issues. Inspired by these considerations, in this paper we provide a comprehensive overview of state-of-the-art temporal big data management proposals, and criticisms on benefits and limitations of these initiatives. We complement our contributions with a deep discussion on future research directions in this area
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
Full text linkModel 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
Logic-based Technologies for Multi-agent Systems: Summary of a Systematic Literature Review
Full text linkThe paper summarises a systematic literature review (SLR) over logic-based technologies for MAS
- …
