Browsing by Author "Malik, Robi"
Now showing items 151 of 51

A framework for compositional nonblocking verification of extended finitestate machines
Mohajerani, Sahar; Malik, Robi; Fabian, Martin (Springer, 20160301)This paper presents a framework for compositional nonblocking verification of discrete event systems modelled as extended finitestate machines (EFSM). Previous results are improved to consider general conflictequivalence ... 
An algorithm for the synthesis of least restrictive controllable supervisors for extended finitestate 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 finitestate 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 memoryefficient supervisors for large discrete event systems, which are least restrictive, controllable, and nonblocking. The approach combines compositional synthesis and ... 
Advanced selfloop removal in compositional nonblocking verification of discrete event systems
Malik, Robi (IEEE, 2015)This paper investigates possible improvements of abstraction to simplify finitestate machines during compositional nonblocking verification of large discrete event systems. Current methods to simplify finitestate machines ... 
Progressive events in supervisory control and compositional verification
Ware, Simon; Malik, Robi (201408)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 coobservability in discreteevent systems
Liu, Huailiang; Leduc, Ryan J.; Malik, Robi; Ricker, S.L. (IEEE, 2014)Existing strategies for verifying coobservability, 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 finitestate 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 finitestate machines (EFSM). Previous results about finitestate machines in lockstep synchronisation ... 
Compositional nonblocking verification with always enabled events and selflooponly events
Pilbrow, Colin; Malik, Robi (Springer, 20131029)This paper proposes to improve compositional nonblocking verification through the use of always enabled and selflooponly events. Compositional verification involves abstraction to simplify parts of a system during ... 
Partial unfolding for compositional nonblocking verification of extended finitestate machines
Mohajerani, Sahar; Malik, Robi; Fabian, Martin (University of Waikato, Department of Computer Science, 20130130)This working paper describes a framework for compositional nonblocking veriﬁcation of reactive systems modelled as extended ﬁnitestate 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 Finitestate 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, 20120919)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, 20120730)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, 201203)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 processalgebraic semantics for generalised nonblocking.
Ware, Simon; Malik, Robi (Australian Computer Society, Inc., 201201)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 ... 
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 ... 
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 ... 
Conflictpreserving 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 ... 
Hierarchical interfacebased supervisory control using the conflict preorder
Malik, Robi; Leduc, Ryan (The international Federation of Automatic Control, 2012)Hierarchical InterfaceBased Supervisory Control decomposes a large discrete event system into subsystems linked to each other by interfaces, facilitating the design of complex systems and the reuse of components. By ... 
Three variations of observation equivalence preserving synthesis abstraction
Mohajerani, Sahar; Malik, Robi; Ware, Simon; Fabian, Martin (University of Waikato, Department of Computer Science, 20110126)In a previous paper we introduced the notion of synthesis abstraction, which allows efficient compositional synthesis of maximally permissive supervisors for largescale systems of composed finitestate automata. In the ... 
Nonblocking and safe control of discreteevent 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, ... 
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 largescale systems of composed finitestate automata. In the ... 
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, 20100707)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 ... 
Modeldriven GUI & interaction design using emulation
Hinze, Annika; Bowen, Judy; Wang, Yuting; Malik, Robi (ACM, 2010)This paper introduces a modeldriven 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, 20090901)This working paper proposes a compositional approach to verify the generalised nonblocking property of discreteevent 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 discreteevent 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 (20080512)A twopass algorithm for compositional synthesis of modular supervisors for largescale systems of composed finitestate 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 ... 
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 finitestate machines satisfies a given safety ... 
Yet another approach to compositional synthesis of discrete event systems
Malik, Robi; Flordal, Hugo (IEEE, 2008)A twopass algorithm for compositional synthesis of modular supervisors for largescale systems of composed finitestate automata is proposed. The first pass provides an efficient method to determine whether a supervisory ... 
Modular synthesis of discrete controllers
Malik, Petra; Malik, Robi; Streader, David; Reeves, Steve (200707)This paper presents supervisory control theory in a processalgebraic 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 discreteevent 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 (200607)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 finitestate machines. Instead, ... 
Modular controlloop detection
Malik, Robi; Malik, Petra (200607)This paper presents an efficient algorithm to detect controlloops in large finitestate 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 serviceoriented architecture: Interaction design.
Hinze, Annika; Malik, Petra; Malik, Robi (20050101)This paper describes our experience when applying formal methods in the design of the tourist information system TIP, which presents contextsensitive 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 ... 
Fair testing revisited: A processalgebraic characterisation of conflicts
Malik, Robi; Streader, David; Reeves, Steve (Springer, Berlin, 2004)This paper studies conflicts from a processalgebraic 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 ... 
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, ... 
Incremental verification and synthesis of discreteevent systems guided by counterexamples
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. (200106)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 finitestring languages and finitestate automata. Properties are verified with respect to ... 
Automated deduction of finitestate control programs for reactive systems
Malik, Robi (Springer, Berlin, 1998)We propose an approach towards the automatic synthesis of finitestate reactive control programs from purely declarative, logic specifications of their requirements. More precisely, if P is a set of propositional temporal ...
Coauthors for Robi Malik
Robi Malik has 30 coauthors in Research Commons.
 Knut Akesson
 Judy Bowen
 Bertil A. Brandin
 H. J. Bravo
 José E. R. Cury
 Petra Dietrich
 Martin Fabian
 Hugo Flordal
 Annika Hinze
 R. Kumar
 S. Lafortune
 Ryan Leduc
 Ryan J. Leduc
 Huailiang Liu
 Petra Malik
 Sahar Mohajerani
 R. Muhlfeld
 L. Ouedraogo
 Patricia N. Pena
 Colin Pilbrow
 Steve Reeves
 S.L. Ricker
 Partha S. Roop
 David Streader
 Marcelo Teixeira
 Yuting Wang
 Simon Ware
 W. M. Wonham
 A. E. C. da Cunha
 Max. H. de Queiroz
Supervised by Robi Malik
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 ...