Synthesizing Distinguishing Formulae for Real Time Systems

Jens Chr. Godskesen
Kim G. Larsen

December 1994


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.


Last modified: 2003-06-08 by webmaster.