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

Znaleziono wyników: 5

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 Verification of Linear-Time Temporal Properties for Reaction Systems with Discrete Concentrations
Męski A., Koutny M., Penczek W.
Fundamenta Informaticae
|
2017
|
Vol. 154, nr 1/4
289--306
EN
Reaction systems are a formal model for computational processes inspired by the functioning of the living cell. This paper introduces reaction systems with discrete concentrations, which are an extension of reaction systems allowing for quantitative modelling. We demonstrate that although reaction systems with discrete concentrations are semantically equivalent to the original qualitative reaction systems, they provide much more succinct representations in terms of the number of entities being used. We define a variant of Linear Time Temporal Logic interpreted over models of reaction systems with discrete concentrations. We provide its suitable encoding in SMT, together with bounded model checking, and present experimental results demonstrating the scalability of the verification method for reaction systems with discrete concentrations.
2
Content available Model Checking Temporal Properties of Reaction Systems
Męski A., Penczek W., Rozenberg G.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2014
|
Nr 1028
1--28
EN
This paper defines a temporal logic for reaction systems (RSTL). The logic is interpreted over the models for the context restricted reaction systems that generalize standard reaction systems by controlling context sequences. Moreover, a translation from the context restricted reaction systems into boolean functions is defined in order to be used for a symbolic model checking for RSTL over these systems. Finally, model checking for RSTL is proved to be PSPACE-complete.
PL
Praca wprowadza logikę temporalną dla systemów reakcyjnych (RSTL), która jest interpretowana w modelach dla systemów reakcyjnych z ograniczeniami kontekstów. Systemy te uogólniają standardowe systemy reakcyjne przez wprowadzenie ograniczeń kontrolujących dopuszczalne konteksty. Ponadto, przedstawiono translację z systemów reakcyjnych z ograniczeniami kontekstów do formuł boolowskich, która umożliwia symboliczną weryfikację modelową dla tych systemów oraz RSTL. Wykazano również, że problem weryfikacji modelowej dla RSTL jest problemem PSPACE-zupełnym.
3
Content available remote SMT-Based Reachability Checking for Bounded Time Petri Nets
Półrola A., Cybula P., Męski A.
Fundamenta Informaticae
|
2014
|
Vol. 135, nr 4
467--482
EN
Time Petri nets by Merlin and Farber are a powerful modelling formalism. However, symbolic model checking methods for them consider in most cases the nets which are 1-safe, i.e., allow the places to contain at most one token. In our paper we present an approach which applies symbolic verification to testing reachability for time Petri nets without this restriction. We deal with the class of bounded nets restricted to disallow multiple enabledness of transitions, and present the method of reachability testing based on a translation into a satisfiability modulo theory (SMT).
4
Content available remote BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets
Męski A., Penczek W., Półrola A.
Fundamenta Informaticae
|
2011
|
Vol. 109, nr 3
305-321
EN
In the paper we present a bounded model checking for 1-safe Petri nets and properties expressed in LTL and the universal fragment of CTL, based on binary decision diagrams. The presented experimental results show that we have obtained a technique which performs better in some of the considered cases, in comparison with the existing SAT-based implementation. The results are also compared with standard BDD-based symbolic method.
5
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
PL
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).
EN
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).
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ć.