From Timed Automata to Logic - and Back
François Laroussinie January 1995 |
Abstract:One of the most successful techniques for automatic
verification is that of model checking. For finite automata there exist
since long extremely efficient model-checking algorithms, and in the last
few years these algorithms have been made applicable to the verification of
real-time automata using the region-techniques of Alur and Dill. In this
paper, we continue this transfer of existing techniques from the setting of
finite (untimed) automata to that of timed automata. In particular, a timed
logic
Available as PostScript, PDF, DVI. |