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

Znaleziono wyników: 55

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

help Ogranicz wyniki do:
first rewind previous Strona / 3 next fast forward last
1
Content available remote TripICS-a Web Service Composition System for Planning Trips and Travels
Niewiadomski A., Switalski P., Kowalczyk M., Penczek W.
Fundamenta Informaticae
|
2018
|
Vol. 157, nr 4
403--425
EN
We present the web service composition system TripICS, which allows for an easy and user-friendly planning of visits to interesting cities and places around the world in combination with travels, arranged in the way satisfying the user’s requirements. TripICS is a specialization of the concrete planning of PlanICS viewed as a constrained optimization problem to the ontology containing services provided by hotels, airlines, railways, museums etc. The system finds an optimal plan by applying a modification of the most efficient concrete planner of PlanICS based on a combination of an SMT-solver with the algorithm GEO. The modification has been designed in order to solve quickly multiple equality constraints. The efficiency of the new planning algorithm is proved by experimental results.
2
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.
3
Content available Towards partial order reductions for fragments of alternating-time temporal logic
Dembiński P., Jamroga W., Mazurkiewicz A., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2016
|
Nr 1036
1--32
EN
A general semantics of strategic abilities of agents in asynchronous systems with and without perfect information is proposed, and some general complexity results for verification of strategic abilities in asynchronous systems are presented. A methodology for partial order reduction (POR) in verification of agents with imperfect information is developed, based on the notion of traces introduced by Mazurkiewicz. Two semantics of ATL∗ −X are considered and it is shown that for memoryless imperfect information (|=ir) contrary to memoryless perfect information (|=Ir), one can apply techniques known for LTL−X.
PL
Raport definiuje ogólną semantykę dla strategicznych umiejętności agentów w systemach asynchronicznych z pełną i częściową informacją, oraz prezentuje ogólne wyniki dotyczące złożoności weryfikacji strategicznych możliwości w systemach asynchronicznych. Metoda redukcji częścio-porządkowych, wykorzystująca ślady Mazurkiewicza, została zastosowana do weryfikacji agentów z niepełną informacją. Dla rozważanych dwóch semantyk logiki ATL*_x zostało pokazane, że dla bezpamięciowej niepełnej informacji (|=ir) w przeciwieństwie do bezpamięciowej pełnej informacji (|=Ir), można zastosować metody znane dla LTL_x.
4
Content available remote Concrete Planning in PlanICS Framework by Combining SMT with GEO and Simulated Annealing
Niewiadomski A., Skaruz J., Switalski P., Penczek W.
Fundamenta Informaticae
|
2016
|
Vol. 147, nr 2/3
289--313
EN
The paper deals with the concrete planning problem – a stage of the web service composition in the PlanICS framework. We present several known and new methods of concrete planning including those based on Satisfiability Modulo Theories (SMT), Genetic Algorithm (GA), as well as methods combining SMT with GA and other nature-inspired algorithms such as Simulated Annealing (SA) and Generalised Extremal Optimization (GEO). The discussion of all the approaches is supported by the complexity analysis, extensive experimental results, and illustrated by a running example.
5
Content available Combining SMT and Simulated Annealing into a Hybrid Planning Method
Skaruz J., Niewiadomski A., Penczek W.
Studia Informatica : systems and information technology
|
2015
|
Vol. 1-2(19)
43--48
EN
We present a new approach to the concrete planning (CP) - a stage of theWeb service composition in the PlanICS framework. A new hybrid algorithm (HSA) based on a combination of Simulated Annealing (SA) with Satisfiability Modulo Theories (SMT) has been designed and implemented. The main idea of our hybrid solution is to use an SMT-based procedure in order to generate an initial individual and then improve it during subsequent iterations of SA. The experimental results show that HSA is superior to the other methods we have applied to the CP problem, including Genetic Algorithm, an SMT-based approach, and our previously developed hybrids.
6
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.
7
Content available remote SMT Versus Genetic and OpenOpt Algorithms : Concrete Planning in the PlanICS Framework
Niewiadomski A., Skaruz J., Penczek W., Szreter M., Jarocki M.
Fundamenta Informaticae
|
2014
|
Vol. 135, nr 4
451--466
EN
The paper deals with the concrete planning problem (CPP) – a stage of the Web Service Composition (WSC) in the PlanICS framework. The complexity of the problem is discussed. A novel SMT-based approach to CPP is defined and its performance is compared to the standard Genetic Algorithm (GA) and the OpenOpt numerical toolset planner in the framework of the PlanICS system. The discussion of all the approaches is supported by extensive experimental results.
8
Content available remote Parameter Synthesis for Timed Kripke Structures
Knapik M., Penczek W.
Fundamenta Informaticae
|
2014
|
Vol. 133, nr 2/3
211--226
EN
We show how to synthesise parameter values under which a given property, expressed in a certain extension of CTL, called RTCTLP, holds in a parametric timed Kripke structure. We prove the decidability of parameter synthesis for RTCTLP by showing how to restrict the infinite space of parameter valuations to its finite subset and employ a brute-force algorithm. The bruteforce approach soon becomes intractable, therefore we propose a symbolic algorithm for RTCTLP parameter synthesis. Similarly to the fixed-point symbolic model checking approach, we introduce special operators which stabilise on the solution. The process of stabilisation is essentially a translation from the RTCTLP parameter synthesis problem to a discrete optimization task. We show that the proposedmethod is sound and complete and provide some complexity results. We argue that this approach leads to new opportunities in model checking, including the use of integer programming and related tools.
9
Content available Solving the abstract planning problem using genetic algorithms
Skaruz J., Niewiadomski A., Penczek W.
Studia Informatica : systems and information technology
|
2013
|
Vol. 1-2(17)
29--48
EN
The paper presents a new approach based on genetic algorithms to the abstract planning problem, which is the first stage of the web service composition problem. An abstract plan is defined as an equivalence class of sequences of service types that satisfy a user query. Intuitively, two sequences are equivalent if they are composed of the same service types, but not necessarily occurring in the same order. The objective of our genetic algorithm (GA) is to return representatives of abstract plans without generating all the equivalent sequences. The paper presents experimental results compared with the results obtained from SMT-solver, which show that GA finds solutions for very large sets of service types in a reasonable time.
10
Content available remote Towards Automated Abstract Planning Based on a Genetic Algorithm
Skaruz J., Niewiadomski A., Penczek W.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2012
|
Nr 1026
1--32
EN
The paper presents a new approach based on nature inspired algorithms to an automated abstract planning problem, which is a part of the web service composition problem. An abstract plan is defined as an equivalence class of sequences of service types that satisfy a user query. Intuitively, two sequences are equivalent if they are composed of the same service types, but not necessarily occurring in the same order. The objective of our genetic algorithm (GA) is to return representatives of abstract plans without generating all the equivalent sequences. The paper presents experimental results, which show that GA finds solutions for very large sets of service types in a reasonable time.
PL
Raport przedstawia nowe podejście do problemu planowania abstrakcyjnego za pomocą algorytmów genetycznych (AG). Problem planowania abstrakcyjnego polega na takiej kompozycji usług sieciowych, która spełnia zapytanie użytkownika. W raporcie pokazano sposób zastosowania AG do rozwiązania problemu planowania abstrakcyjnego oraz zaprezentowano wyniki eksperymentalne.
11
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.
12
Content available remote Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems
Penczek W., Woźna-Szcześniak B., Zbrzezny A.
Fundamenta Informaticae
|
2012
|
Vol. 119, nr 3/4
373-392
EN
This paper makes two contributions to the verification of multi-agent systems modelled by interleaved interpreted systems. Firstly, the paper presents theoretical underpinnings of the SATbased bounded model checking (BMC) approach for LTL extended with the epistemic component (LTLK) over interleaved interpreted systems. Secondly, the BMC method has been implemented and tested on several benchmarks for MAS. The preliminary experimental results reveal advantages and disadvantages of our SAT-based BMC for LTLK and show that the method has a significant potential.
13
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.
14
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.
15
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.
16
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.
17
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.
18
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.
19
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.
20
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).
first rewind previous Strona / 3 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ć.