Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Powiadomienia systemowe

Sesja wygasła!

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: Computational Tree Logic

Sortuj według:

Ogranicz wyniki do:

Model Checking for Graded CTL

Ferrante A., Napoli M., Parente M.

Fundamenta Informaticae

2009

Vol. 96, nr 3

323-339

Recently, complexity issues related to the decidability of the μ-calculus, when the universal and existential quantifiers are augmented with graded modalities, have been investigated by Kupfermann, Sattler and Vardi ([19]). Graded modalities refer to the use of the universal and existential quantifiers with the added capability to express the concept of at least k or all but k, for a non-negative integer k. In this paper we study the Computational Tree Logic CTL, a branching time extension of classical modal logic, augmented with graded modalities and investigate the complexity issues with respect to the model-checking problem. We consider a system model represented by a Kripke structure K and give an algorithm to solve the model-checking problem running in time [...] which is hence tight for the problem (here φ is the number of temporal and boolean operators and does not include the values occurring in the graded modalities). In this framework, the graded modalities express the ability to generate a user-defined number of counterexamples to a specification φgiven in CTL. However, these multiple counterexamples can partially overlap, that is they may share some behavior. We have hence investigated the case when all of them are completely disjoint. In this case we prove that the model-checking problem is both NP-hard and coNP-hard and give an algorithm for solving it running in polynomial space. We have thus studied a fragment of graded-CTL, and have proved that the model-checking problem is solvable in polynomial time.

Modelowanie i weryfikacja protokołu SCTP z wykorzystaniem automatów czasowych ze zmiennymi

Męski A., Półrola A.

Zeszyty Naukowe Wyższej Szkoły Informatyki

2008

Vol. 7, Nr 1

49-67

W pracy konstruujemy model protokołu SCTP (Stream Transmission Control Protocol) - protokołu transportowego zawierającego szereg mechanizmów mających zapewnić niezawodne dostarczanie. Do modelowania protokołu używamy automatów czasowych ze zmiennymi całkowitymi. Otrzymany model wykorzystywany jest następnie do automatycznej weryfikacji protokołu, podczas której testujemy własności wyrażone za pomocą formuł logiki temporalnej CTL (ang. Computation Tree Logic).

In the paper we construct a model for SCTP (Stream Control Transmission Protocol) - a transport layer protocol which provides mechanisms of reliable delivery. The protocol is modelled by a set of timed automata augmented with integer variables. The resulting model is then used to test the protocol w.r.t. certain properties expressed by the formulas of the temporal logic CTL (Computation Tree Logic).