Wyniki wyszukiwania - Biblioteka Nauki

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

Znaleziono wyników: 5

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Bounded Model Cheking for Interpreted Systems

100%

Penczek W. , Lomuscio A.

tom Nr 946

1-8

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

W pracy przedstawiamy rozszerzenie algorytmu ograniczonej weryfikacji modelowej do temporalnych formuł epistemicznych. Algorytm jest zastosowany do weryfikacji pewnego wariantu problemu transmisji bitów.

First-Order Linear-time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment

100%

Belardinelli F. , Lomuscio A.

tom Vol. 106, nr 2-4

175-190

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.

Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems

80%

Lomuscio A. , Penczek W. , Qu H.

tom Vol. 101, nr 1/2

71-90

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.

Model Checking Optimisation Based Congestion Control Algorithms

80%

Lomuscio A. , Strulo B. , Walker N. G. , Wu P.

2010

tom Vol. 102, nr 1

77-96

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.

Runtime Monitoring of Contract Regulated Web Services

80%

Lomuscio A. , Penczek W. , Solanki M. , Szreter M.

tom Vol. 111, nr 3

339-353

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.