Research Commons

Browsing by Author "Malik, Robi"

Research Commons

Browsing by Author "Malik, Robi"

Sort by: Order: Results:

  • Mohajerani, Sahar; Malik, Robi; Fabian, Martin (University of Waikato, Department of Computer Science, 2013)
    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 ...
  • Mohajerani, Sahar; Malik, Robi; Fabian, Martin (University of Waikato, Department of Computer Science, 2013)
    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 ...
  • 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 ...
  • 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 ...
  • Mohajerani, Sahar; Malik, Robi; Fabian, Martin (University of Waikato, Department of Computer Science, 2012)
    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 ...
  • Mohajerani, Sahar; Malik, Robi; Fabian, Martin (University of Waikato, Department of Computer Science, 2012)
    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 ...
  • Ware, Simon; Malik, Robi (Australian Computer Society, Inc., 2012)
    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 ...
  • 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 ...
  • 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 ...
  • 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 ...
  • 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 ...
  • 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 ...
  • Mohajerani, Sahar; Malik, Robi; Ware, Simon; Fabian, Martin (University of Waikato, Department of Computer Science, 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 ...
  • 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 ...
  • 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, ...
  • 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 ...
  • Malik, Robi (University of Waikato, Department of Computer Science, 2010)
    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 ...
  • Hinze, Annika; Bowen, Judith Alyson; 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 ...
  • Malik, Robi; Leduc, Ryan (University of Waikato, Department of Computer Science, 2009)
    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 ...
  • 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 ...
  • Malik, Robi; Flordal, Hugo (2008)
    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 ...
  • 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 ...
  • 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 ...
  • 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 ...
  • Malik, Petra; Malik, Robi; Streader, David; Reeves, Steve (2007)
    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 ...
  • 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 ...
  • 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 ...
  • Malik, Robi; Malik, Petra (2006)
    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 ...
  • Malik, Robi; Flordal, Hugo (2006)
    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, ...
  • 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 ...
  • 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 ...
  • Hinze, Annika; Malik, Petra; Malik, Robi (2005)
    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 ...
  • 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 ...
  • 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, ...
  • 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 ...
  • 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 ...
  • 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 ...
  • Malik, Robi; Dietrich, Petra; Wonham, W. M.; Brandin, Bertil A. (2001)
    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 ...
  • 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 ...
  • 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 ...

Co-authors for Robi Malik

Supervised by Robi Malik

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

  • 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 ...