### Skapa referens, olika format (klipp och klistra)

**Harvard**

Voronov, A. och Åkesson, K. (2009) *Verification of Supervisory Control Properties of Finite Automata Extended with Variables*. Göteborg : Chalmers University of Technology (R - Department of Signals and Systems, Chalmers University of Technology, nr: 003/2009).

** BibTeX **

@techreport{

Voronov2009,

author={Voronov, Alexey and Åkesson, Knut},

title={Verification of Supervisory Control Properties of Finite Automata Extended with Variables},

abstract={Verification and synthesis of control logic programs using Supervisory Control Theory (SCT) is an important topic. Most SCT methods are based on finite state automata (FA). FA extended with variables (EFA) are a compact, but otherwise equivalent to FA notation, proven to be beneficial in modeling control logic systems. To use existing SCT methods with EFA, it is necessary to convert EFA to FA. In certain cases this conversion can be very time-consuming, even if the number of resulting reachable states is very small compared to the total state-set of the system. In this paper we present a way to do verification of SCT properties of EFA models without converting them to FA. Instead, we convert them to the models for Symbolic Model Verification tool NuSMV. The conversion is performed in polynomial time. Experimental results show that NuSMV effectively utilizes small reachable state-set of the system to do verification.},

publisher={Chalmers University of Technology},

place={Göteborg},

year={2009},

series={R - Department of Signals and Systems, Chalmers University of Technology, no: 003/2009},

keywords={formal verification, supervisory control, finite automata, manufacturing systems, control logic, model checking},

note={6},

}

** RefWorks **

RT Report

SR Electronic

ID 94442

A1 Voronov, Alexey

A1 Åkesson, Knut

T1 Verification of Supervisory Control Properties of Finite Automata Extended with Variables

YR 2009

AB Verification and synthesis of control logic programs using Supervisory Control Theory (SCT) is an important topic. Most SCT methods are based on finite state automata (FA). FA extended with variables (EFA) are a compact, but otherwise equivalent to FA notation, proven to be beneficial in modeling control logic systems. To use existing SCT methods with EFA, it is necessary to convert EFA to FA. In certain cases this conversion can be very time-consuming, even if the number of resulting reachable states is very small compared to the total state-set of the system. In this paper we present a way to do verification of SCT properties of EFA models without converting them to FA. Instead, we convert them to the models for Symbolic Model Verification tool NuSMV. The conversion is performed in polynomial time. Experimental results show that NuSMV effectively utilizes small reachable state-set of the system to do verification.

PB Chalmers University of Technology

T3 R - Department of Signals and Systems, Chalmers University of Technology, no: 003/2009

LA eng

LK http://publications.lib.chalmers.se/records/fulltext/94442.pdf

OL 30