 |
|
|||
| Authors: | Karsten Strehl |
| Group: | Computer Engineering |
| Type: | Techreport |
| Title: | Using Interval Diagram Techniques for the Symbolic Verification of Timed Automata |
| Year: | 1998 |
| Month: | July |
| Pub-Key: | Str98 |
| Keywords: | SMC IDD |
| Rep Nbr: | 53 |
| Institution: | Computer Engineering and Networks Lab (TIK), Swiss Federal Institute of Technology (ETH) Zurich |
| Abstract: | In this report, we suggest interval diagram techniques for formal verification of timed automata. Interval diagram techniques are based on interval decision diagrams (IDDs) – representing sets of system configurations of, e.g., timed automata – and interval mapping diagrams (IMDs) – modeling their transition behavior. IDDs are canonical representations of Boolean functions and allow for their efficient manipulation. We present the methods necessary for our approach and compare its results to another, similar verification technique. |
| Remarks: | TIK Report No. 53, July 1998 |
| Resources: | [BibTeX] [Paper as PDF] |
