ca.mcgill.lmp.finite
Class Bisim

java.lang.Object
  extended byca.mcgill.lmp.finite.Bisim

public class Bisim
extends java.lang.Object

Bisim encapsulates all the information required to run the bisim() algorithm. It also contains the method getLumpedLMP() that build a lumped LMP using the information produced by bisim(). A common usage would be:
Bisim bisim = new Bisim(myLMP);
bisim.bisim();
LMP lumpedLMP = bisim.getLumpedLMP;
System.out.println("result: " + lumpedLMP.toString();

Author:
Alexandre Bouchard

Constructor Summary
Bisim(LMP lmp)
          Create an instance of LMP to lump the given lmp.
 
Method Summary
 void bisim()
          This algorithm allows us to distinguish states that do not satisfy the same formulas in the following logic:
L0 :== T | f_1 ^ f_2 | q f
This logic has the property to characterize bisimulation: two states are bisimilar iff they satisfy the same formulas in L0.
 java.util.Set getD1()
          See bisim().
 java.util.Map getFormulas()
          A way to obtain the formulas as a map indexed by the sets of D1 and mapped to the formula in L0 (a String) that all the states in the given set satisfy.
 LMP getLumpedLMP()
          After the execution of bisim(), Bisim has all the infomation required to compute a simplified, "lumped" LMP.
static void main(java.lang.String[] args)
          bisim [optionalArguments] <inputFile>
Bisim takes the description of a LMP as input and outputs a LMP obtained by quotienting the input LMP by the equivalence relation of bisimulation
First argument: the path to a file describing a LMP
Optional arguments:
  --transitions Output the transition matrices of the new LMP
  --sets Output the set D1 used in an intermediate step
The LMP should be described using the following specification:
The description should be a list of transition matrices (one per label) separated by the "\n*\n" string.
static void printUsage()
          Print in System.err a description of the functionalities of main().
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

Bisim

public Bisim(LMP lmp)
Create an instance of LMP to lump the given lmp. This lmp will not be modified.

Parameters:
lmp -
Method Detail

bisim

public void bisim()
This algorithm allows us to distinguish states that do not satisfy the same formulas in the following logic:
L0 :== T | f_1 ^ f_2 | q f
This logic has the property to characterize bisimulation: two states are bisimilar iff they satisfy the same formulas in L0. Beginning with D1 containing only the set of all states, bisim operates as follow: for each label a in the set of labels and B2 in D1, it ``splits'' every set B1 of D1 into subsets having the same probability of jumping to B2 with action a; this is done until it does not modify D1. At the end, all states satisfying the same formulas will belong to exactly the same sets in D1.

From: J. Desharnais, A. Edalat, P. Panangaden, Bisimulation for Labelled Markov Processes


getD1

public java.util.Set getD1()
See bisim().

Returns:
The set D1 that bisim() computed.

getFormulas

public java.util.Map getFormulas()
A way to obtain the formulas as a map indexed by the sets of D1 and mapped to the formula in L0 (a String) that all the states in the given set satisfy.
See bisim() and split().

Returns:
The map of formulas

getLumpedLMP

public LMP getLumpedLMP()
After the execution of bisim(), Bisim has all the infomation required to compute a simplified, "lumped" LMP. Indeed, the sets in D1=D2 represent (after the execution of bisim) formulas in a logic s.t. 2 states are bisimilar iff they belong to the sets in D1. So the sets in D1 can be viewed as binary partitions of the states, and the first step to compute the lumped LMP is to compute the union of those partitions. The second step is to compute the transition matrices with straightforward additions of probabilities. A new LMP is finally created with those informations and returned.
Note: A rather suboptimal way to do that but we don't care about the time complexity and implementation of this method. "Premature optimization is the root of all evil." --D. Knuth

Returns:
The lumped LMP

main

public static void main(java.lang.String[] args)
bisim [optionalArguments] <inputFile>
Bisim takes the description of a LMP as input and outputs a LMP obtained by quotienting the input LMP by the equivalence relation of bisimulation
First argument: the path to a file describing a LMP
Optional arguments:
  --transitions Output the transition matrices of the new LMP
  --sets Output the set D1 used in an intermediate step
The LMP should be described using the following specification:
The description should be a list of transition matrices (one per label) separated by the "\n*\n" string. The transition matrices should be formated by separating columns by tabs and rows by new lines characters.

Parameters:
args -

printUsage

public static void printUsage()
Print in System.err a description of the functionalities of main().
See main().