PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 13

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Runtime Monitoring of Contract Regulated Web Services
Lomuscio A., Penczek W., Solanki M., Szreter M.
Fundamenta Informaticae
|
2011
|
Vol. 111, nr 3
339-353
EN
We investigate the problem of locally monitoring contract regulated behaviours in agentbased web services. We encode contract clauses in service specifications by using extended timed automata. We propose a non intrusive local monitoring framework along with an API to monitor the fulfillment (or violation) of contractual obligations. A key feature of the framework is that it is fully symbolic thereby providing a scalable solution to monitoring. At runtime execution steps generated by the service are passed as input to the runtime monitor. Conformance of the execution against the service specification is checked using a symbolically represented extended timed automaton. This allows us to monitor service behaviours over large state spaces generated by multiple, long running contracts. We illustrate our methodology by monitoring a service composition scenario from the vehicle repair domain, and report on the experimental results.
2
Content available remote Model Checking Temporal-Epistemic Logic Using Alternating Tree Automata
Belardinelli F., Jones A. V., Lomuscio A.
Fundamenta Informaticae
|
2011
|
Vol. 112, nr 1
19-37
EN
We introduce a novel automata-theoretic approach for the verification of multi-agent systems. We present epistemic alternating tree automata, an extension of alternating tree automata, and use them to represent specifications in the temporal-epistemic logic CTLK. We show that model checking a memory-less interpreted system against a CTLK property can be reduced to checking the language non-emptiness of the composition of two epistemic tree automata. We report on an experimental implementation and discuss preliminary results. We evaluate the effectiveness of the technique using two real-life scenarios: a gossip protocol and the train gate controller.
3
Content available remote First-Order Linear-time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment
Belardinelli F., Lomuscio A.
Fundamenta Informaticae
|
2011
|
Vol. 106, nr 2-4
175-190
EN
We investigate quantified interpreted systems, a computationally grounded semantics for a first-order temporal epistemic logic on linear time. We report a completeness result for themonodic fragment of a language that includes LTL modalities as well as distributed and common knowledge. We exemplify possible uses of the formalismby analysingmessage passing systems, a typical framework for distributed systems, in a first-order setting.
4
Content available remote Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems
Lomuscio A., Penczek W., Qu H.
Fundamenta Informaticae
|
2010
|
Vol. 101, nr 1/2
71-90
EN
We investigate partial order reduction techniques for the verification of multi-agent systems. We investigate the case of 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 in the system. 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 implementations and the experimental results obtained against well-known examples in the MAS literature.
5
Content available remote Model Checking Optimisation Based Congestion Control Algorithms
Lomuscio A., Strulo B., Walker N.G., Wu P.
Fundamenta Informaticae
|
2010
|
Vol. 102, nr 1
77-96
EN
Model checking has been widely applied to the verification of network protocols. Alternatively, optimisation based approaches have been proposed to reason about the large scale dynamics of networks, particularly with regard to congestion and rate control protocols such as TCP. This paper intends to provide a first bridge and explore synergies between these two approaches. We consider a series of discrete approximations to the optimisation based congestion control algorithms. Then we use branching time temporal logic to specify formally the convergence criteria for the system dynamics and present results from implementing these algorithms on a state-of-the-art model checker. We report on our experiences in using the abstraction of model checking to capture features of the continuous dynamics typical of optimisation based approaches.
6
Content available remote LDYIS: a Framework for Model Checking Security Protocols
Lomuscio A., Penczek W.
Fundamenta Informaticae
|
2008
|
Vol. 85, nr 1-4
359-375
EN
We present a formalism for the automatic verification of security protocols based on multi-agent systems semantics. We give the syntax and semantics of a temporal-epistemic security-specialised logic and provide a lazy-intruder model for the protocol rules that we argue to be particularly suitable for verification purposes. We exemplify the technique by finding a (known) bug in the traditional NSPK protocol.
7
Content available remote Model checking security protocols : a multi-agent system approach
Lomuscio A., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2007
|
Nr 1000
1-23
EN
We present a formalism for the automatic verification of security protocols based on multi-agent systems semantics. We give syntax and semantics of a temporal-epistemic security-specialised logie and provide a lazy-intruder model for the protocol rules that is arguably particularly suitable for verification purposes. We exemplify the techniąue by finding a (known) bug in the traditional NSPK protocol
PL
Praca prezentuje nowe podejście do automatycznej weryfikacji protokołów kryptograficznych, bazujące na semantyce systemów wieloagentowych. Podajemy składnię i semantykę temporalno-epistemicznej logiki dla protokołów kryptograficznych oraz model intruza typu "lazy", który jest szczególnie właściwy dla celów weryfikacji. Nasza technika jest przedstawiona na przykladzie protokołu NSPK, dla którego znajdujemy znany atak.
8
Content available remote Verification of the Tesla protocol in Mcmas-x
Lomuscio A., Raimondi F., Woźna B.
Fundamenta Informaticae
|
2007
|
Vol. 79, nr 3-4
473-486
EN
We use Mcmas-x to verify authentication properties in the Tesla secure stream protocol. Mcmas-xis an extension to explicit and deductive knowledge of the Obdd-based model checker Mcmas a verification tool for multi-agent systems.
9
Content available remote Comparing BDD and SAT based techniques for model checking Chaum's Dining Cryptographers Protocol
Kacprzak M., Lomuscio A., Niewiadomski A., Penczek W., Raimondi F., Szreter M.
Fundamenta Informaticae
|
2006
|
Vol. 72, nr 1-3
215-234
EN
We analyse different versions of the Dining Cryptographers protocol by means of automatic verification via model checking. Specifically we model the protocol in terms of a network of communicating automata and verify that the protocol meets the anonymity requirements specified. Two different model checking techniques (ordered binary decision diagrams and SAT-based bounded model checking) are evaluated and compared to verify the protocols.
10
Content available remote From Bounded to Unbounded Model Checking for Temporal Epistemic Logic
Kacprzak M., Lomuscio A., Penczek W.
Fundamenta Informaticae
|
2004
|
Vol. 63, nr 2,3
221--240
EN
This paper addresses the problem of verification of temporal epistemic properties of multi-agent systems by means of symbolic model checking. An overview of the technique of bounded model checking for temporal epistemic logic, and an analysis of some limitations of the method are provided. An extension of this technique called unbounded model checking to solve these limitations is explored. Similarities and differences of the two methods are explicitly exemplified by the analysis of a scenario in the two formalisms.
11
Content available remote Unbounded Model Checking for Knowledge and Time
Kacprzak M., Lomuscio A., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2003
|
Nr 966
1-27
EN
We present an approach to the problem of verification of epistemic properties in multi-agent systems by means of symbolic model checking. In particular, it isshown how to extend the technique of unbounded model checking from a purely temporal setting to a temporal-epistemic one. In order to achieve this, we baseour discussion on interpreted systems semantics, a popular semantics used in multi-agent systems literature. We give details of the technique and show howit can be applied to the well known train, gate and controller problem.
PL
Nieograniczona weryfikacja modelowa dla systemów z wiedzą i czasem. Praca dotyczy problemu weryfikacji epistemicznych własności systemów wieloagentowych za pomocą symbolicznej weryfikacji modelowej. Pokazujemy jak poszerzyć technikę zwaną nieograniczoną weryfikacją modelową stosowaną do badania temporalnych własności systemów tak, aby można było ją wykorzystać również do analizowania epistemicznych własności. W tym celu bazujemy na interpretowanych systemach - popularnej semantyce szeroko opisywanej w literaturze dotyczącej systemów wieloagentowych. Podajemy szczegóły techniki oraz demonstrujemy zastosowanie jej do znanego problemu kontroli przejazdów kolejowych.
12
Content available remote Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking
Penczek W., Lomuscio A.
Fundamenta Informaticae
|
2003
|
Vol. 55, nr 2
167-185
EN
We present a framework for verifying temporal and epistemic properties of multi-agent systems by means of bounded model checking. We use interpreted systems as underlying semantics. We give details of the proposed technique, and show how it can be applied to the ``attacking generals problem'', a typical example of coordination in multi-agent systems.
13
Content available remote Bounded Model Cheking for Interpreted Systems
Penczek W., Lomuscio A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2002
|
Nr 946
1-8
EN
We present an extension of a bounded model checking algorithm to deal with temporal epistemic formulas. We use the algorithm to solve a variant of the bit transmission problem
PL
W pracy przedstawiamy rozszerzenie algorytmu ograniczonej weryfikacji modelowej do temporalnych formuł epistemicznych. Algorytm jest zastosowany do weryfikacji pewnego wariantu problemu transmisji bitów.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.