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

Znaleziono wyników: 3

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  reachability problem
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
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.
2
Content available remote Solvability of the Halting and Reachability Problem for Binary 2-tag Systems
De Mol L.
Fundamenta Informaticae
|
2010
|
Vol. 99, nr 4
435-471
EN
In this paper a detailed proofwill be given of the solvability of the halting and reachability problem for binary 2-tag systems.
3
Content available remote Checking Reachability Properties for Timed Automata via SAT
Woźna B., Penczek W., Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2002
|
Nr 949
1-19
EN
The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded to the depth k Î N and encoded as a prepositional formula. Next the desired property is translated to a prepositional formula and the satisfiability of the conjunction of the two above defined formulas is checked. The unfolding of the transition can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results. Keywords : Reachability problem, bounded model checking, translation to SAT, Timed Automata, Augmented Region Graphs, discretization.
PL
Testowanie osiągalności automatów czasowych z wykorzystaniem SAT. Praca opisuje nowe podejście do problemu osiągalności dla automatów czasowych. Główna idea polega na połączeniu znanego algorytmu przeszukującego przestrzeń stanów wszerz metodą BFS oraz metody ograniczonej weryfikacji modelowej. Aby sprawdzić, czy stan spełniający daną własność jest osiągalny w modelu dla rozważanego automatu czasowego postępujemy następująco. Rozwijamy stopniowo relację przejścia dla automatu, aż do głębokości k Î N i kodujemy ją jako formułę zdaniową. Następnie, za pomocą formuły zdaniowej kodowana jest rozważana własność i sprawdzana jest spełnialność koniunkcji obydwu zdefiniowanych formuł zdaniowych. Rozwijanie relacji przejścia może zostać zakończone jeśli poszukiwany stan został znaleziony lub wszystkie stany danego automatu czasowego zostały przeszukane.
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ć.