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

Znaleziono wyników: 11

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 Extrapolation of an Optimal Policy using Statistical Probabilistic Model Checking
Rataj A., Woźna-Szcześniak B.
Fundamenta Informaticae
|
2018
|
Vol. 157, nr 4
443--461
EN
We present different ways of an approximate extrapolation of an optimal policy of a small model to that of a large equivalent of the model, which itself is too large to find its exact policy directly using probabilistic model checking (PMC). In particular, we obtain a global optimal resolution of non-determinism in several small Markov Decision Processes (MDP) or its extensions like Stochastic Multi-player Games (SMG) using PMC. We then use that resolution to form a hypothesis about an analytic decision boundary representing a respective policy in an equivalent large MDP/SMG. The resulting hypothetical decision boundary is then statistically approximately verified, if it is locally optimal and if it indeed represents a “good enough” policy. The verification either weakens or strengthens the hypothesis. The criterion of the optimality of the policy can be expressed in any modal logic that includes a version of the probabilistic operator P~p[·], and for which a PMC method exists.
2
Content available A GPGPU–based simulator for prism: statistical verification of results of PMC
Copik M., Rataj A., Woźna-Szcześniak B.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2017
|
Vol. 22
85--97
EN
We describe a GPGPU–based Monte Carlo simulator integrated with Prism. It supports Markov chains with discrete or continuous time and a subset of properties expressible in PCTL, CSL and their variants extended with rewards. The simulator allows an automated statistical verification of results obtained using Prism’s formal methods.
3
Content available remote SMT-based Searching for κ-quasi-optimal Runs in Weighted Timed Automata
Woźna-Szcześniak B., Zbrzezny A. M., Zbrzezny A.
Fundamenta Informaticae
|
2017
|
Vol. 152, nr 4
411--433
EN
We investigate a quasi-optimal cost reachability problem for weighted timed automata. We use a translation to the satisfiability modulo theories (SMT) problem to solve the problem. In particular, we show how to find a run of length κ ∊ N that starts at the initial state and terminates at a state containing the target location, its total cost belongs to the interval [c; c + 1), for some natural number c ∊ IN, and the cost of each other run of length κ, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of run is called κ-quasi-optimal. We exemplify the use of our solution to the investigated problem by means of the weighted timed generic pipeline protocol and the weighted job shop scheduling problem, and we provide some preliminary experimental results.
4
Content available On the SMT-based verification of communicative commitments
Woźna-Szcześniak B., Szcześniak I.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2016
|
Vol. 21
161--187
EN
We propose an SMT-based bounded model checking (BMC) technique for the existential fragments of CCTL*K – an epistemic temporal logic extended to include modalities for different social commitments – and for multi-agent systems modelled by Communication Interpreted Systems (CIS). Furthermore, we exemplify the use of the technique by means of the NetBill protocol, a popular example in the MAS literature related to the modelling of business processes.
5
Content available remote SAT-based Bounded Model Checking for Weighted Deontic Interpreted Systems
Woźna-Szcześniak B.
Fundamenta Informaticae
|
2016
|
Vol. 143, nr 1/2
173--205
EN
We present WECTL*KD, a weighted branching time temporal logic to specify knowledge, and correct functioning behaviour in multi-agent systems (MAS).We interpret the formulae of the logic over models generated by weighted deontic interpreted systems (WDIS). Furthermore, we investigate a SAT-based bounded model checking (BMC) technique for WDIS and for WECTL*KD.
6
Content available SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties
Woźna-Szcześniak B., Szcześniak I.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2015
|
Vol. 20
69--81
EN
We define an SAT-based bounded model checking (BMC) method for RTECTLK (the existential fragment of the real-time computation tree logic with knowledge) that is interpreted over timed models generated by timed interpreted systems. Specifically, we translate the model checking problem for RTECTLK to the model checking problem for a variant of branching temporal logic (called EyCTLK) interpreted over an abstract model, and we redefine an SAT-based BMC technique for EyCTLK.
7
Content available remote Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
Woźna-Szcześniak B., Zbrzezny A.
Fundamenta Informaticae
|
2014
|
Vol. 135, nr 4
553--568
EN
We investigate a SAT-based bounded model checking (BMC) method for MTL (metric temporal logic) that is interpreted over linear discrete infinite time models generated by discrete timed automata. In particular, we translate the existential model checking problem for MTL to the existential model checking problem for a variant of linear temporal logic (called HLTL), and we provide a SAT-based BMC technique for HLTL. We show how to implement the BMC technique for HLTL and discrete timed automata, and as a case study we apply the technique in the analysis of GTPP, a Generic Timed Pipeline Paradigm modelled by a network of discrete timed automata.
8
Content available remote A Translation of the Existential Model Checking Problem from MITL to HLTL
Woźna-Szcześniak B., Zbrzezny A.
Fundamenta Informaticae
|
2013
|
Vol. 122, nr 4
401--420
EN
In the paper we propose a translation of the existential model checking problemfor timed automata and properties expressible in MITL to the existential model checking problem for HLTL. Such a translation, for example, allows to adopt LTL bounded model checking method for verification of the MITL properties
9
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.
10
Content available Verifying RTECTL properties of a train controller systems
Woźna-Szcześniak B., Zbrzezny A., Zbrzezny Andrzej
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2011
|
Vol. 16
153--162
EN
In the paper we deal with a classic concurrency problem - a faulty train controller system (FTC). In particular, we formalize it by means of finite automata, and consider several properties of the problem, which can be expressed as formulae of a soft real-time branching time temporal logic, called RTECTL. Further, we verify the RTECTL properties of FTC by means of SAT-based bounded model checking (BMC) method, and present the performance evaluation of the BMC method with respect to the considered problem. The performance evaluation is given by means of the running time and the memory used.
11
Content available SAT-based searching for k-quasi-optimal runs in weighted timed automata
Woźna-Szcześniak B., Zbrzezny A.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2010
|
Vol. 15
163--176
EN
In the paper we are concerned with an optimal cost reachability problem for weighted timed automata, and we use a translation to SAT to solve the problem. In particular, we show how to find a run of length k ∈ IN that starts at the initial state and terminates at a state containing a target location, its total cost belongs to the interval [c,c+1), for some natural number c ∈ IN, and the cost of each other run of length k, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of runs is called k-quasi-optimal. We exemplify the use of our solution to the mentioned problem by means of the air traffic control problem, and we provide some preliminary experimental results.
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ć.