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:  graf regionów
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote SAT-Based Bounded Model Checking for the Universal Fragment of TCTL
EN
Bounded Model Checking (BMC) based on SAT methods consists in searching for a counterexample of a particular length and to generate a propositional formula that is satisfiable iff such a counterexample exists. Our paper shows how the concept of bounded model checking can be extended to deal with \TACTL\ (the universal fragment of \TCTL ) properties of a network of concurrent Timed Automata.
PL
Ograniczona Weryfikacja Modelowa, bzaująca na metodach SAT, polega na poszukiwaniu kontrprzykładów o długości ograniczonej przez pewną liczbę całkowitą k > 0 oraz generowanie formuły zdaniowej, która jest spełniana wtedy i tylko wtedy, gdy taki kontrprzykład istnieje. Celem tej pracy jest przedstawienie koncepcji ograniczonej weryfikacji modelowej dla automatów czasowych reprezentowanych przez siec współbieżnych i wzajemnie komunikujących się komponentów oraz własności wyrażanych w języku logiki TACTL (uniwersalnego fragmentu TCTL).
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ć.