Now showing items 11-15 of 18

  • On the use of observation equivalence in synthesis abstraction

    Mohajerani, Sahar; Malik, Robi; Ware, Simon; Fabian, Martin (IEEE, 2011)
    In a previous paper we introduced the notion of synthesis abstraction, which allows efficient compositional synthesis of maximally permissive supervisors for large-scale systems of composed finite-state automata. In the ...
  • Partial unfolding for compositional nonblocking verification of extended finite-state machines

    Mohajerani, Sahar; Malik, Robi; Fabian, Martin (University of Waikato, Department of Computer Science, 2013-01-30)
    This working paper describes a framework for compositional nonblocking verification of reactive systems modelled as extended finite-state machines. The nonblocking property can capture the absence of livelocks and deadlocks ...
  • Supremica – An integrated environment for verification, synthesis and simulation of discrete event systems

    Akesson, Knut; Fabian, Martin; Flordal, Hugo; Malik, Robi (IEEE, 2006)
    An integrated environment, Supremica, for verification, synthesis and simulation of discrete event systems is presented. The basic model in Supremica is finite automata where the transitions have an associated event together ...
  • Supremica-An Efficient Tool for Large-Scale Discrete Event Systems

    Malik, Robi; Akesson, Knut; Flordal, Hugo; Fabian, Martin (Elsevier, 2017)
    Supremica is a tool for the modelling and analysis of discrete-event control functions based on state machine models of the uncontrolled plant and specification of the desired closed-loop behaviour. The modelling framework ...
  • Synthesis equivalence of triples

    Mohajerani, Sahar; Malik, Robi; Fabian, Martin (University of Waikato, Department of Computer Science, 2012-09-19)
    This working paper describes a framework for compositional supervisor synthesis, which is applicable to all discrete event systems modelled as a set of deterministic automata. Compositional synthesis exploits the modular ...