Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 1

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

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Checking Reachability Properties for Timed Automata via SAT
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ć.