2012 Working Papers
Permanent URI for this collection
Recent Submissions
Item Synthesis equivalence of triples(Working Paper, University of Waikato, Department of Computer Science, 2012-09-19) Mohajerani, Sahar; Malik, Robi; Fabian, MartinThis 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 structure of the input model, and therefore works best for models consisting of a large number of small automata. State-space explosion is mitigated by the use of abstraction to simplify individual components, and the property of synthesis equivalence guarantees that the final synthesis result is the same as it would have been for the non-abstracted model. The working paper describes synthesis equivalent abstractions and shows their use in an algorithm to compute supervisors efficiently. The algorithm has been implemented in the DES software tool Supremica and successfully computes modular supervisors, even for systems with more than 1014 reachable states, in less than 30 seconds.Item Synthesis observation equivalence and weak synthesis observation equivalence(Working Paper, University of Waikato, Department of Computer Science, 2012-07-30) Mohajerani, Sahar; Malik, Robi; Fabian, MartinThis working paper proposes an algorithm to simplify automata in such a way that compositional synthesis results are preserved in every possible context. It relaxes some requirements of synthesis observation equivalence from previous work, so that better abstractions can be obtained. The paper describes the algorithm, adapted from known bisimulation equivalence algorithms, for the improved abstraction method. The algorithm has been implemented in the DES software tool Supremica and has been used to compute modular supervisors for several large benchmark examples. It successfully computes modular supervisors for systems with more than 10¹² reachable states.Item Five abstraction rules to remove transitions while preserving compositional synthesis results(Working Paper, University of Waikato, Department of Computer Science, 2012-03) Mohajerani, Sahar; Malik, Robi; Fabian, MartinThis working paper investigates under which conditions transitions can be removed from an automaton while preserving important synthesis properties. The work is part of a framework for compositional synthesis of least restrictive controllable and nonblocking supervisors for modular discrete event systems. The method for transition removal complements previous results, which are largely focused on state merging. Issues concerning transition removal in synthesis are discussed, and redirection maps are introduced to enable a supervisor to process an event, even though the corresponding transition is no longer present in the model. Based on the results, different techniques are proposed to remove controllable and uncontrollable transitions, and an example shows the potential of the method for practical problems.Item A simulation study of the use of electric vehicles as storage on the New Zealand electricity grid(Working Paper, University of Waikato, Department of Computer Science, 2012-04) Monigatti, Paul; Apperley, Mark; Rogers, BillThis paper describes a simulation to establish the extent to which reliance on non-dispatchable energy sources, most typically wind generation, could in the future be extended beyond received norms, by utilizing the distributed battery capacity of an electric vehicle fleet. The notion of exploiting the distributed battery capacity of a nation’s electric vehicle fleet as grid storage is not new. However, this simulation study specifically examines the potential impact of this idea in the New Zealand context. The simulation makes use of real and projected data in relation to vehicle usage, full potential non-dispatchable generation capacity and availability, taking into account weather variation, and typical daily and seasonal patterns of usage. It differs from previous studies in that it is based on individual vehicles, rather than a bulk battery model. At this stage the analysis is aggregated, and does not take into account local or regional flows. A more detailed analysis of these localized effects will follow in subsequent stages of the simulation.