Bisimulation - Finite Labelled Markov Processes (LMP)

Summary

This package is an implementation of the bisimulation algorithm in [DEP], a modification of Cleaveland's algorithm [Cle]. It gives a way to distinguish states that do not satisfy the same formulas in a minimalist logic (L0). The main use of that is to simplify LMP's by grouping bisimilar state (to "lump" bisimilar states). See [DEP] for more information on bisimilarity, the L0 logic, the proof of characterization of bisimilarity by the L0 logic and the proof of correctness of the algorithm.

Documentation

• Usage: cd to the bin/ directory and type:
  java ca.mcgill.lmp.finite.Bisim -h
  
• Test cases: cd to the bin/ directory. There are examples of LMP descriptions in the LMP_descriptions/ directory (1.lmp, ..., 4.lmp). Invoque them using:
  java ca.mcgill.lmp.finite.Bisim ../LMP_descriptions/1.lmp
  The output should be (for 1.lmp):
  Input:
  Number of states: 4
  States: s2 s1 s3 s0
  Output (lumped LMP):
  Number of states: 2
  States: [s1, s3] [s2, s0]
  Try 4.lmp for a more complex example. The output in this case should be:
  Input:
  Number of states: 10
  States: s2 s4 s9 s8 s6 s1 s3 s7 s5 s0
  Output (lumped LMP):
  Number of states: 4
  States: [s6, s0] [s1, s7] [s4, s9, s5] [s2, s8, s3]
• Javadoc documentation

References

• [DEP]: J. Desharnais, A. Edalat, P. Panangadent, Bisimulation for Labelled Markov Processes,
• [Cle]: R. Cleaveland, On automatic explaining bisimulation inequivalence. In E.M. Clarke and R.P. Kurshan, editors, Computer-Aided Verification CAV 90, number 531 in Lecture Notes in Computer Science, page 364-372, 1990.