|
Synthesizing Distinguishing Formulae for Real Time Systems
Jens Chr. Godskesen December 1994 |
Abstract:This paper describes a technique for generating diagnostic information for the timed bisimulation equivalence and the timed simulation preorder. More precisely, given two (parallel) networks of regular real-time processes, the technique will provide a logical formula that differentiates them in case they are not timed (bi)similar. Our method may be seen as an extension of the algorithm by for deciding timed bisimilarity in that information of time-quantities has been added sufficient for generating distinguishing formulae. The technique has been added to the automatic verification tool EPSILON and applied to various examples. Available as PostScript, PDF, DVI. |