Browsing by Author "Malik, Robi"

Ware, Simon; Malik, Robi
(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 ...

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

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

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

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

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

Pilbrow, Colin; Malik, Robi
(Springer, 2013)
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 ...

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 veriﬁcation of reactive systems modelled as extended ﬁnitestate machines. The nonblocking property can capture the absence of livelocks and deadlocks ...

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

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

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

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

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

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; 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 largescale systems of composed finitestate 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 largescale systems of composed finitestate 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, 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 ...

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 discreteevent 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 discreteevent systems. Generalised nonblocking is introduced in to overcome weaknesses of the standard nonblocking check in ...

Malik, Robi; Flordal, Hugo
(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 ...

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

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

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

Malik, Petra; Malik, Robi; Streader, David; Reeves, Steve
(2007)
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 ...

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

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; Malik, Petra
(2006)
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 ...

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 finitestate 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 contextsensitive 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; 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 ...

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

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 finitestring languages and finitestate automata. Properties are verified with respect to ...

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
Supervised by Robi Malik