AbstractThis 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 Cerans for deciding timed bisimilarity in that information of time-quantities has been added sufficient for generating distinguishing formulae.
Categories and Subject Descriptors: D.2.2 [Software Engineering]: Tools and Techniques; D.2.4 [Software Engineering]: Program Verification; F.1.2 [Computation by Abstract Devices]: Modes of Computation; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages
Additional Key Words and Phrases: tools and techniques, verification, process algebra, real time
Selected references
- Rocco De Nicola and Frits Vaandrager. Three logics for branching bisimulation (extended abstract). In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 118-129, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.