PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników
Powiadomienia systemowe
  • Sesja wygasła!
  • Sesja wygasła!

Znaleziono wyników: 15

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 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).
2
Content available remote SMT-based Abstract Planning in PlanICS Ontology
Niewiadomski A., Penczek W., Półrola A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2012
|
Nr 1027
1--42
EN
The paper deals with the abstract planning problem - the first stage of Web Service Composition (WSC) in the Planics framework. We present a solution based on a compact repre-sentation of abstract plans by multisets of service types and a reduction of the planning problem to a task for an SMT-solver. The paper presents theoretical aspects of the abstract planning as well as some details of our symbolic encoding and implementation, followed by preliminary experimental results.
PL
Przedmiotem niniejszej pracy jest problem planowania abstrakcyjnego - pierwszy etap kompozycji usług sieciowych w systemie Planics. Prezentujemy rozwiązanie bazujące na kompaktowej reprezentacji planów abstrakcyjnych za pomocą wielozbiorów typów usług i redukcji problemu planowania do problemu spełnialności instancji SMT (Satisfiability Modulo Theories). Przedstawiamy zarówno teoretyczne aspekty planowania, jak również szczegóły symbolicznego kodowania i implementacji oraz wstępne wyniki eksperymentalne.
3
Content available remote Towards Automatic Composition of Web Services : SAT-Based Concretisation of Abstract Scenarios
Niewiadomski A., Penczek W., Półrola A., Szreter M., Zbrzezny A.
Fundamenta Informaticae
|
2012
|
Vol. 120, nr 2
181-203
EN
Automating the composition of web services is an object of a growing interest. In our paper [13] we proposed a method for converting the problem of the composition to the problem of building a graph of worlds consisting of formally defined objects, and presented the first phase of this composition aimed at building a graph of types of services (an abstract graph). In this work we propose a method of replacing abstract flows of this graph by sequences of concrete services able to satisfy the user’s request. The method is based on SAT-based reachability checking for (timed) automata with discrete data and parametric assignments.
4
Content available remote PlanICS - a Web Service Composition Toolset
Doliwa D., Horzelski W., Niewiadomski A., Penczek W., Półrola A., Szreter M., Zbrzezny A.
Fundamenta Informaticae
|
2011
|
Vol. 112, nr 1
47-71
EN
The paper presents a prototype toolset to planning by automatic composition of web services. The main idea consists in arranging the composition into two main phases: abstract and concrete one, as well as to handle fully declarative user queries. The first abstract stage aims at finding all the possible sequences of the types of the services that can potentially satisfy the user request. The result, referred to as an abstract plan, is used in the concrete planning phase, which substitutes the types of the services with their concrete instances registered in the system. This is obtained by translating the problem of finding a composition of concrete services satisfying the user query into the reachability problem for (timed) automata with discrete data and parametric assignments, taking into account the concrete instances of services as well as the user query. Next, SAT-based parametric bounded model checking is used to obtaining the solutions in form of sequences of services invocations together with the example services' input values.
5
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.
6
Content available Web Services composition - from ontology to plan by query
Doliwa D., Horzelski W., Jarocki M., Niewiadomski A., Penczek W., Półrola A., Szreter M.
Control and Cybernetics
|
2011
|
Vol. 40, no 2
315-336
EN
The paper proposes a method to cover the world of web services with a uniform semantics, possibly simple but enabling to arrange complex flows of service invocations. The flows are built according to fully declarative user's intentions, specified in a language common for the descriptions of services and for the query. In the approach we model the world of services and of the subjects they operate on using a uniform knowledge database and an objectoriented manner. The current work describes the first phase of the composition: making an abstract plan, i.e., giving an answer how (with what types of services) the required effect can be obtained. The problem of creating a plan is converted to building a specialized graph.
7
Content available remote Towards automatic composition of web services :
Jarocki M., Niewiadomski A., Penczek W., Półrola A., Szreter M.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2010
|
Nr 1017
1-40
EN
The paper proposes a method of converting the problem of automated composition of web services to the problem of building a graph of worlds consisting of formally defined objects. We present basic rules of defining ontologies for services execution environments, in which automatic reasoning about sequences of service calls leading to saatisfying a user's intention is possible. The intention can be specified in a fully declarative language, without knowledge about services. In turn, the services are treated as independent "black boxes", realizing their activities regardless of the flow in which they attend. The intentions and the descriptions of the services are the only source of knowledge used to generate abstract plans. The above planning process is the first phase of automated composition. The paper presents also a tool implementing our composition algorithm and some experimental results.
PL
Praca zawiera propozycję konwersji zagadnienia automatycznej kompozycji usług sieciowych do problemu budowy grafu światów zbudowanych z formalnie zdefiniowanych obiektów. Przedstawiono podstawy budowy ontologii środowiska wykonania usług, w której możliwe jest automatyczne wnioskowanie przebiegu wywołań, prowadzących do realizacji intencji użytkownika. Język wyrażania takiej intencji jest całkowicie deklaratywny i wraz z ontologią, w której usługi pozostają nie związanymi ze sobą "czarnymi skrzynkami", stanowi jedyne źródło wiedzy dla budowy abstrakcyjnych planów wykonania. Opisany tutaj proces stanowi pierwszą z trzech faz automatycznej kompozycji, będącej tematem badań zespołu. Praca prezentuje również narzędzie implementujące algorytm kompozycji oraz przykład jego zastosowania.
8
Content available remote Bounded Parametric Verification for Distributed Time Petri Nets with Discrete-Time Semantics
Knapik M., Penczek W., Szreter M., Półrola A.
Fundamenta Informaticae
|
2010
|
Vol. 101, nr 1/2
9-27
EN
Bounded Model Checking (BMC) is an efficient technique applicable to verification of temporal properties of (timed) distributed systems. In this paper we show for the first time how to apply BMC to parametric verification of time Petri nets with discrete-time semantics. The properties are expressed by formulas of the logic PRTECTL - a parametric extension of the existential fragment of Computation Tree Logic (CTL).
9
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).
10
Content available remote VerICS 2007 - a Model Checker for Knowledge and Real-Time
Kacprzak M., Nabiałek W., Niewiadomski A., Penczek W., Półrola A., Szreter M., Woźna B., Zbrzezny A.
Fundamenta Informaticae
|
2008
|
Vol. 85, nr 1-4
313-328
EN
The papers presents the current stage of the development of VerICS - a model checker for real-time and multi-agent systems. Depending on the type of a system considered, it enables to test various classes of properties - from reachability to temporal, epistemic and deontic formulas. The model checking methods used to this aim include both SAT-based and enumerative ones. In the paper we focus on new features of the verifier: SAT-based model checking for multi-agent systems and several extensions and improvements to real-time systems' verification.
11
Content available remote SAT-Based Reachability Checking for Timed Automata with Discrete Data
Zbrzezny A., Półrola A.
Fundamenta Informaticae
|
2007
|
Vol. 79, nr 3-4
579-593
12
Content available remote Minimization Algorithms for Time Petri Nets
Półrola A., Penczek W.
Fundamenta Informaticae
|
2004
|
Vol. 60, nr 1-4
307--331
EN
The paper presents three methods for applying partitioning algorithms, used for generating abstract models for timed automata, to the case of time Petri nets. Each of these methods is based on a different approach to the concrete semantics of a net, and can potentially be more efficient than the others in a particular case. Besides the theoretical description, we provide some preliminary experimental results, obtained from the implementation integrated with the model checking tool VeriCS.
13
Content available remote Reachability Analysis for Timed Automata Based on Partitioning
Półrola A., Penczek W., Szreter M.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2003
|
Nr 961
1-23
EN
Model checking is an approach commonly applied for automated verification of reachability properties. Given a system $S$ and a property $p$, reachability model checking consists in an exploration of the state space of $S$, checking whether there exists a state where $p$ holds. Since concrete state spaces (models) of timed systems are usually infinite, they cannot be directly applied to model checking. One of the solution to this problem is to exploit finite abstract models, preseving the properties of interest. The paper presents a new method of buildng abstract models for Timed Automata, based on a partitioning algorithm. Our pseudo-bisimulating models are often smaller than forward-reachability graphs , commonly used in reachability analysis. The method enables verification on-the-fly, i.e., generating of the model can be stopped as soon as a state satisfying $p$ is found.
PL
Automatyczne testowanie osiągalności wykonywane jest zazwyczaj za pomocą metod weryfikacji modelowej. Dla danego systemy S i właściwości p polega ono na przejrzeniu przestrzeni stanów S i sprawdzeniu, czy zawiera ona stan w którym p zachodzi. Istotne znaczenie ma zatem rozmiar przeglądanej przestrzeni (modelu), który w wielu przypadkach (np. dla systemów z czasem) może być nawet nieskończony. Jednym z możliwych rozwiązań jest zastosowanie skończonych modeli abstrakcyjnych zachowujących żądane własności. Praca przedstawia nową metodę generowania modeli abstrakcyjnych dla automatów czasowych, bazujących na algorytmie minimalizacji (podziału). Otrzymywane modele pseudobisymulacyjne zachowują osiągalność, a przy tym są często mniejsze niż używane zwykle do jej testowania tzw. grafy forward-reachability. Metoda pozawala też na wykonywanie weryfikacji "w locie", tj. przerywanie budowania modelu gdy wygenerowany zostanie stan spełniający p.
14
Content available remote Reachability Analysis for Timed Automata Using Partitioning Algorithms
Półrola A., Penczek W., Szreter M.
Fundamenta Informaticae
|
2003
|
Vol. 55, nr 2
203-221
EN
The paper presents a new method for checking reachability properties of Timed Automata. The idea consists in on-the-fly verification of a property on a pseudo-bisimulating model generated by a modified partitioning algorithm. Pseudo-bisimulating models are often much smaller than forward-reachability graphs commonly used in reachability analysis. A theoretical description of the algorithm is supported by several experimental results.
15
Content available remote Verification of Timed Automata Based on Similarity
Dembiński P., Penczek W., Półrola A.
Fundamenta Informaticae
|
2002
|
Vol. 51, nr 1,2
59-89
EN
The paper presents a modification of the standard partitioning technique to generate abstract state spaces preserving similarity for Timed Automata. Since this relation is weaker than bisimilarity, most of the obtained models (state spaces) are smaller than bisimilar ones, but still preserve the universal fragments of branching time temporal logics. The theoretical results are exemplified for strong, delay, and observational simulation relations.
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ć.