|
| << vorige | volgende >> |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 6 van 12 gevonden artikelen
| Titel: |
Bounded Model Checking for the Existential Fragment of TCTL_{-G} and Diagonal Timed Automata |
| Auteur: |
Woźna, Bożena Zbrzezny, Andrzej |
| Verschenen in: |
Fundamenta informaticae |
| Paginering: | Jaargang 79 (2007) nr. 1-2 pagina's 229-256 |
| Jaar: |
2007-09-13 |
| Inhoud: |
Bounded Model Checking (BMC) is one of the well known SAT based symbolic model checking techniques. It consists in searching for a counterexample of a particular length, and generating a propositional formula that is satisfiable iff such a counterexample exists. The BMC method is feasible for the various classes of temporal logic; in particular it is feasible for TECTL (the existential fragment of Time Computation Tree Logic) and Diagonal-free Timed Automata. The main contribution of the paper is to show that the concept of Bounded Model Checking can be extended to deal with TECTL_{-G} properties of Diagonal Timed Automata. We have implemented our new BMC algorithm, and we present preliminary experimental results, which demonstrate the efficiency of the method. |
| Uitgever: |
IOS Press |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 6 van 12 gevonden artikelen
| << vorige | volgende >> |