Michael Jones, PhD

vocabulary:

• Controllable linear system: a linear control system is
  x(t+1) = Ax(t) + Bu(t)
  where x is a vector description of the system state, u is the inputs and A,B are matrices of rational (or real) numbers. Such a system is controllable if every state is reachable from every other state [MDJ: very interesting implications for modeling as Buchi automata and should simplify the detection of accept states in cycles--if that's the way they go with this] The translation of a controllable linear system to a transition system (using the definition below) is pretty straightforward except for the definition of the observation space and mapping which are defined as part of the abstraction.
  
• quotient system
  
• denumerable set
  
• quotient system on a denumerable set
  
• bisimilar: there is an simulation relation and an inverse simulation relation between two transition systems. A and B are bisimilar if B mimics every move of A forward and backward. (p 5) Bisimilation implies languages are equal. Language equivalence preserves interpretation of LTL formulae (and mu-calculus in general for that matter).
  
• bisimilar quotient
  
• 
  

What is the main contribution?