Now showing items 1-53 of 53

  • A framework for compositional nonblocking verification of extended finite-state machines

    Mohajerani, Sahar; Malik, Robi; Fabian, Martin (Springer, 2016-03-01)
    This paper presents a framework for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results are improved to consider general conflict-equivalence ...
  • An algorithm for the synthesis of least restrictive controllable supervisors for extended finite-state machines

    Malik, Robi; Teixeira, Marcelo (Department of Computer Science, The University of Waikato, 2016)
    This working paper proposes an algorithm for the synthesis of modular supervisors using extended finite-state machines, i.e., state machines with variables and guards on the transitions. Synthesis is performed by iteratively ...
  • Compositional supervisor synthesis with state merging and transition removal

    Mohajerani, Sahar; Malik, Robi; Fabian, Martin (Department of Computer Science, The University of Waikato, 2016)
    This working paper proposes a framework to obtain memory-efficient supervisors for large discrete event systems, which are least restrictive, controllable, and nonblocking. The approach combines compositional synthesis and ...
  • Programming a fast explicit conflict checker

    Malik, Robi (IEEE, 2016)
    This paper describes the implementation of explicit model checking algorithms to verify the nonblocking or nonconflicting property of discrete event systems. Explicit algorithms enumerate and store all reachable states of ...
  • An algorithm for compositional nonblocking verification using special events

    Pilbrow, Colin; Malik, Robi (Elsevier Science, 2015-12-01)
    This paper proposes to improve compositional nonblocking verification of discrete event systems through the use of special events. Compositional verification involves abstraction to simplify parts of a system during ...
  • Advanced selfloop removal in compositional nonblocking verification of discrete event systems

    Malik, Robi (IEEE, 2015)
    This paper investigates possible improvements of abstraction to simplify finite-state machines during compositional nonblocking verification of large discrete event systems. Current methods to simplify finite-state machines ...
  • Progressive events in supervisory control and compositional verification

    Ware, Simon; Malik, Robi (2014-08)
    This paper investigates some limitations of the nonblocking property when used for supervisor synthesis in discrete event systems. It is shown that there are cases where synthesis with the nonblocking property gives undesired ...
  • Certainly Unsupervisable States

    Ware, Simon; Malik, Robi; Mohajerani, Sahar; Fabian, Martin (Springer International Publishing, 2014)
    This paper proposes an abstraction method for compositional synthesis. Synthesis is a method to automatically compute a control program or supervisor that restricts the behaviour of a given system to ensure safety and ...
  • Verification of the observer property in discrete event systems

    Pena, Patricia N.; Bravo, H. J.; da Cunha, A. E. C.; Malik, Robi; Lafortune, S.; Cury, José E. R. (Institute of Electrical and Electronics Engineers Inc., 2014)
    The observer property is an important condition to be satisfied by abstractions of Discrete Event System (DES) models. This technical note presents a new algorithm that tests if an abstraction of a DES obtained through ...
  • Incremental verification of co-observability in discrete-event systems

    Liu, Huailiang; Leduc, Ryan J.; Malik, Robi; Ricker, S.L. (IEEE, 2014)
    Existing strategies for verifying co-observability, one of the properties that must be satisfied for synthesizing solutions to decentralized supervisory control problems, require the construction of the complete system ...
  • Supervisory control with progressive events

    Ware, Simon; Malik, Robi (IEEE, 2014)
    This paper investigates some limitations of the nonblocking property when used for supervisor synthesis in discrete event systems. It is shown that there are cases where synthesis with the nonblocking property gives undesired ...
  • An algorithm for compositional nonblocking verification of extended finite-state machines

    Mohajerani, Sahar; Malik, Robi; Fabian, Martin (IFAC, 2014)
    This paper describes an approach for compositional nonblocking verification of discrete event systems modelled as extended finite-state machines (EFSM). Previous results about finite-state machines in lock-step synchronisation ...
  • Compositional nonblocking verification with always enabled events and selfloop-only events

    Pilbrow, Colin; Malik, Robi (Springer, 2013-10-29)
    This paper proposes to improve compositional nonblocking verification through the use of always enabled and selfloop-only events. Compositional verification involves abstraction to simplify parts of a system during ...
  • 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 ...
  • Variable abstraction and approximations in supervisory control synthesis

    Teixeira, Marcelo; Malik, Robi; Cury, José E. R.; de Queiroz, Max. H. (IEEE, 2013)
    This paper proposes a method to simplify Extended Finite-state Automata (EFA) in such a way the least restrictive controllable supervisor is preserved. The method is based on variable abstraction, which involves the ...
  • Compositional nonblocking verificationusing generalised nonblocking abstractions

    Malik, Robi; Leduc, Ryan (IEEE, 2013)
    This paper proposes a method for compositional verification of the standard and generalized nonblocking properties of large discrete event systems. The method is efficient as it avoids the explicit construction of the ...
  • 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 ...
  • Synthesis observation equivalence and weak synthesis observation equivalence

    Mohajerani, Sahar; Malik, Robi; Fabian, Martin (University of Waikato, Department of Computer Science, 2012-07-30)
    This 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 ...
  • Five abstraction rules to remove transitions while preserving compositional synthesis results

    Mohajerani, Sahar; Malik, Robi; Fabian, Martin (University of Waikato, Department of Computer Science, 2012-03)
    This 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 ...
  • A process-algebraic semantics for generalised nonblocking.

    Ware, Simon; Malik, Robi (Australian Computer Society, Inc., 2012-01)
    Generalised nonblocking is a weak liveness property to express the ability of a system to terminate under given preconditions. This paper studies the notions of equivalence and refinement that preserve generalised nonblocking ...
  • Transition removal for compositional supervisor synthesis

    Mohajerani, Sahar; Malik, Robi; Fabian, Martin (IEEE, 2012)
    This 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 ...
  • Hierarchical interface-based supervisory control using the conflict preorder

    Malik, Robi; Leduc, Ryan (The international Federation of Automatic Control, 2012)
    Hierarchical Interface-Based Supervisory Control decomposes a large discrete event system into subsystems linked to each other by interfaces, facilitating the design of complex systems and the re-use of components. By ...
  • Generalised verification of the observer property in discrete event systems

    Bravo, H. J.; da Cunha, A. E. C.; Pena, Patricia N.; Malik, Robi; Cury, José E. R. (2012)
    The observer property is an important condition to be satisfied by abstractions of Discrete Event Systems (DES) models. This paper presents a generalised version of a previous algorithm which tests if an abstraction of a ...
  • An algorithm for weak synthesis observation equivalence for compositional supervisor synthesis

    Mohajerani, Sahar; Malik, Robi; Fabian, Martin (The international Federation of Automatic Control, 2012)
    This 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 ...
  • Conflict-preserving abstraction of discrete event systems using annotated automata

    Ware, Simon; Malik, Robi (Springer, 2012)
    This paper proposes to enhance compositional verification of the nonblocking property of discrete event systems by introducing annotated automata. Annotations store nondeterministic branching information, which would ...
  • Three variations of observation equivalence preserving synthesis abstraction

    Mohajerani, Sahar; Malik, Robi; Ware, Simon; Fabian, Martin (University of Waikato, Department of Computer Science, 2011-01-26)
    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 ...
  • 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 ...
  • Nonblocking and safe control of discrete-event systems modeled as extended finite automata

    Ouedraogo, L.; Kumar, R.; Malik, Robi; Akesson, Knut (IEEE, 2011)
    Extended Finite Automata (EFA), i.e., finite automata extended with variables, are a suitable modeling framework for discrete event systems owing to their compactness, resulting from the use of variables. In this paper, ...
  • Compositional synthesis of discrete event systems using synthesis abstraction

    Mohajerani, Sahar; Malik, Robi; Ware, Simon; Fabian, Martin (IEEE, 2011)
    This paper proposes a general method to synthesize a least restrictive supervisor for a large discrete event system model, consisting of a large number of arbitrary automata representing the plants and specifications. A ...
  • The language of certain conflicts of a nondeterministic process

    Malik, Robi (University of Waikato, Department of Computer Science, 2010-07-07)
    The language of certain conflicts is the most general set of behaviours of a nondeterministic process, which certainly lead to a livelock or deadlock when accepted by another process running in parallel. It is of great use ...
  • Model-driven GUI & interaction design using emulation

    Hinze, Annika; Bowen, Judy; Wang, Yuting; Malik, Robi (ACM, 2010)
    This paper introduces a model-driven emulator for the interaction and GUI design of complex interacting systems. It allows systems that are engineered using formal methods and modelling to be tested with users before the ...
  • Seven abstraction rules preserving generalised nonblocking

    Malik, Robi; Leduc, Ryan (University of Waikato, Department of Computer Science, 2009-09-01)
    This working paper proposes a compositional approach to verify the generalised nonblocking property of discrete-event systems. Generalised nonblocking is introduced in [15] to overcome weaknesses of the standard nonblocking ...
  • A compositional approach for verifying generalized nonblocking

    Malik, Robi; Leduc, Ryan (IEEE, 2009)
    This paper proposes a compositional approach to verify the generalised nonblocking property of discrete-event systems. Generalised nonblocking is introduced in to overcome weaknesses of the standard nonblocking check in ...
  • Compositional synthesis of discrete event systems via synthesis equivalence

    Malik, Robi; Flordal, Hugo (2008-05-12)
    A two-pass algorithm for compositional synthesis of modular supervisors for largescale systems of composed finite-state automata is proposed. The first pass provides an efficient method to determine whether a supervisory ...
  • Generalised Nonblocking

    Malik, Robi; Leduc, Ryan (IEEE Computer Society, 2008)
    This paper studies the nonblocking check used in supervisory control of discrete event systems and its limitations. Different examples with different liveness requirements are discussed. It is shown that the standard ...
  • Yet another approach to compositional synthesis of discrete event systems

    Malik, Robi; Flordal, Hugo (IEEE, 2008)
    A two-pass algorithm for compositional synthesis of modular supervisors for large-scale systems of composed finite-state automata is proposed. The first pass provides an efficient method to determine whether a supervisory ...
  • The Use of Language Projection for Compositional Verification of Discrete Event Systems

    Ware, Simon; Malik, Robi (IEEE Computer Society, 2008)
    This paper proposes the use of abstraction by language projection to improve the performance of compositional verification to prove or disprove that a large system of composed finite-state machines satisfies a given safety ...
  • Modular synthesis of discrete controllers

    Malik, Petra; Malik, Robi; Streader, David; Reeves, Steve (2007-07)
    This paper presents supervisory control theory in a process-algebraic setting, and proposes a way of synthesising modular supervisors that guarantee nonblocking. The framework used includes the possibility of hiding actions ...
  • Conflicts and projections

    Malik, Robi; Flordal, Hugo; Pena, Patricia N. (2007)
    This paper studies abstraction methods suitable to verify very large models of discrete-event systems to be nonconflicting. It compares the observer property to methods known from process algebra, namely to conflict ...
  • Compositional synthesis of maximally permissive supervisors using supervision equivalence

    Flordal, Hugo; Malik, Robi; Fabian, Martin; Akesson, Knut (Springer Netherlands, 2007)
    This paper presents a general framework for efficient synthesis of supervisors for discrete event systems. The approach is based on compositional minimisation, using concepts of process equivalence. In this context, a large ...
  • Modular nonblocking verification using conflict equivalence

    Malik, Robi; Flordal, Hugo (2006-07)
    This paper proposes a modular approach to verifying whether a large discrete event system is nonconflicting. The new approach avoids computing the synchronous product of a large set of finite-state machines. Instead, ...
  • Modular control-loop detection

    Malik, Robi; Malik, Petra (2006-07)
    This paper presents an efficient algorithm to detect control-loops in large finite-state systems. The proposed algorithm exploits the modular structure present in many models of practical relevance, and often successfully ...
  • Supervision equivalence

    Flordal, Hugo; Malik, Robi (2006)
    This paper presents a general framework for modular synthesis of supervisors for discrete event systems. The approach is based on compositional minimisation, using concepts of process equivalence. Its result is a ...
  • 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 ...
  • Towards a TIP 3.0 service-oriented architecture: Interaction design.

    Hinze, Annika; Malik, Petra; Malik, Robi (2005-01-01)
    This paper describes our experience when applying formal methods in the design of the tourist information system TIP, which presents context-sensitive information to mobile users with small screen devices. The dynamics of ...
  • Adaptive techniques for specification matching in embedded systems: A comparative study

    Malik, Robi; Roop, Partha S. (Springer, Berlin, 2005)
    The specification matching problem in embedded systems is to determine whether an existing component may be adapted suitably to match the requirements of a new specification. Recently, a refinement called forced simulation ...
  • On the set of certain conflicts of a given language

    Malik, Robi (2004)
    Two concurrent processes are said to be in conflict if they can get trapped in a situation where they both are waiting or running endlessly, forever unable to complete their common task. In the design of reactive systems, ...
  • Fair testing revisited: A process-algebraic characterisation of conflicts

    Malik, Robi; Streader, David; Reeves, Steve (Springer, Berlin, 2004)
    This paper studies conflicts from a process-algebraic point of view and shows how they are related to the testing theory of fair testing. Conflicts have been introduced in the context of discrete event systems, where two ...
  • Incremental verification and synthesis of discrete-event systems guided by counter-examples

    Brandin, Bertil A.; Malik, Robi; Malik, Petra (2004)
    This article presents new approaches to system verification and synthesis based on subsystem verification and the novel combined use of counterexamples and heuristics to identify suitable subsystems incrementally. The scope ...
  • A case study in verification of UML statecharts: the PROFIsafe protocol

    Malik, Robi; Muhlfeld, R. (2003)
    We discuss our experience obtained during the PROFIsafe verification and test case generation project at Siemens Corporate Technology. In this project, a formal analysis of the PROFIsafe protocol for failsafe communication ...
  • Implementation considerations in supervisory control

    Malik, Robi; Dietrich, Petra; Wonham, W. M.; Brandin, Bertil A. (2001-06)
    With supervisory control theory it is possible to describe controllers which influence the behaviour of a system by disabling controllable events. But sometimes it is desirable to have a controller which not only disables ...
  • Incremental system verification and synthesis of minimally restrictive behaviours

    Malik, Robi (2000)
    An incremental approach to system verification is proposed, for system behaviours and safety properties described by means of finite-string languages and finite-state automata. Properties are verified with respect to ...
  • Automated deduction of finite-state control programs for reactive systems

    Malik, Robi (Springer, Berlin, 1998)
    We propose an approach towards the automatic synthesis of finite-state reactive control programs from purely declarative, logic specifications of their requirements. More precisely, if P is a set of propositional temporal ...

Showing up to 5 theses - most recently added to Research Commons first.

  • Partial Order Reduction with Compositional Verification

    Shaw, Adrian Mark (University of Waikato, 2014)
    This thesis expands the usage of partial order reduction methods in reducing the state space of large models in model checking. The work done can be divided into two parts. In the first part we introduce two new ample ...
  • On Conflicts in Concurrent Systems

    Ware, Simon Ian (University of Waikato, 2014)
    This dissertation studies conflicts. A conflict is a bug in concurrent systems where one or more components of the system may potentially be blocked from completing their task. This dissertation investigates how nonconflicting ...