# VHS BibTeX archive





@Inproceedings{AE96:ifac ,
author =	 {Appelhaus, P. and Engell, S.},
title =	 {Extended observer for the polymerization of
polyethylenterephtalate},
booktitle =	 {IFAC-World Congress 1996},
year =	 1996,
url =		 {http://www-verimag.imag.fr/VHS/year1/cs21d.ps},
abstract =	 {In the batch polymerization of
polyethylenterephtalate, the main reaction is an
equilibrium-reaction. The removal of ethylenglycol
from the melt determines the velocity of the
polycondensation process, because it shifts the
equilibrium to the side of chain growth. In this
paper, we report about the implementation of an
observer, which is based on a simple polymerization
model at a pilot plant scale reactor. The observer
is able to determine two important concentrations in
the polymer melt as well as the product of mass
transfer coefficient and specific surface. The
knowledge of the later parameter offers new
possibilities for improved process control},
}



@InProceedings{AMPS98:controllersynthesis,
author =	 {E.~Asarin and O.~Maler and A.~Pnueli and J.~Sifakis},
title =	 {Controller Synthesis for Timed Automata},
booktitle =	 {Proc.\ System Structure and Control},
year =	 1998,
organization = {IFAC},
publisher =	 {Elsevier},
month =	 {July},
pages =	 {469-474},
url =
{http://www-verimag.imag.fr/~maler/Papers/newsynth.ps.gz},
abstract =	 {Controller Synthesis for Timed Automata. In this
work we tackle the following problem: given a timed
automaton, restrict its transition relation in a
systematic way so that all the remaining behaviors
satisfy certain properties. This is an extension of
the problem of controller synthesis for discrete
event dynamical systems, where in addition to
choosing among actions, the controller have the
option of doing nothing and let the time pass. The
problem is formulated using the notion of a
real-time game, and a winning strategy is
constructed as a fixed-point of an operator on the
space of states and clock configurations.}
}



@inproceedings{AcLa99,
author =	 "Aceto, Luca and Laroussinie, Fran{\c c}ois",
title =	 "Is your Model Checker on Time? --- On the Complexity
of Model Checking for Timed Modal Logics",
year =	 1999,
series =	 {LNCS},
volume =	 1672,
booktitle =	 "Proc.\ of MFCS 1999",
abstract =	 "This paper studies the structural complexity of
model checking for (variations on) the specification
formalisms used in the tools CMC and Uppaal, and
fragments of a timed alternation-free
$\mu$-calculus. For each of the logics we study, we
characterize the computational complexity of model
checking, as well as its specification and program
complexity, using timed automata as our system
model",
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/AcLa99.ps.gz}
}



@InProceedings{AltisenGoesslerPnueliSifakisTripakisYovine99,
author =	 {K. Altisen and G. Goessler and A. Pnueli and
J. Sifakis and S. Tripakis and S. Yovine},
title =	 {A Framework for Scheduler Synthesis},
booktitle =	 {RTSS 1999 proceedings},
pages =	 {154-163},
year =	 {1999},
editor =	 {IEEE Computer Society},
url =
{http://www-verimag.imag.fr/VHS/resources/agpsty99.ps.gz},
abstract =	 {A framework to integrate specification and scheduler
generation for real-time systems is presented. In a
first step, the system, which can include
or without precedence constraints, any number of
resources and CPUs, ...) is specified in terms of a
timed Petri-net formalism. We show how to generate,
in a second step, the most general non-preemptive
dynamic online scheduler for this specification,
using a controller synthesis technique.}
}



@InProceedings{AltisenGoesslerSifakis2000,
author =	 {K. Altisen and G. Goessler and J. Sifakis},
title =	 {A Methodology for the Construction of Scheduled
Systems},
booktitle =	 {submitted to FTRTFT 2000},
year =	 2000,
url =
{http://www-verimag.imag.fr/VHS/resources/ags2000.ps.gz},
abstract =	 {A methodology for constructing scheduled systems by
restricting successively the behavior of the
processes to be scheduled, is studied. Restriction
is used to guarantee the satisfaction of two types
of constraints: schedulability constraints
guaranteeing that timing properties of the processes
are satisfied, and constraints characterizing
particular scheduling algorithms including process
priorities, non-idling, and preemption. The
methodology is based on a controller synthesis
paradigm. The main results deal with the
characterization of scheduling policies as safety
constraints and the simplification of the synthesis
process by applying a composability principle.}
}



@Unpublished{AltisenNiebert00,
author =	 {Karine Altisen and Peter Niebert},
title =	 {Online Scheduling for VHS Case Study 7 --
Intermediate report},
note =	 {VHS deliverable in Workpackage CS.7.1},
url =		 {http://www-verimag.imag.fr/VHS/CS7/an00.ps.gz},
year =	 2000
}



@Unpublished{AmDaWa00,
author =	 {Tobias Amnell and Alexandre David and Wang Yi},
title =	 {A Real Time Animator for Hybrid Systems},
note =	 {Accepted for in the proceedings of 6th ACM SIGPLAN
LCTES'2000.},
year =	 2000,
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/AmDaWa00.ps.gz}
}



@InProceedings{Asarin98:equations,
author =	 {E.~Asarin},
title =	 {Equations on Timed Languages},
booktitle =	 {Hybrid Systems: Computation and Control},
editor =	 {T.A.~Henzinger and S.~Sastry},
volume =	 1386,
series =	 {LNCS},
year =	 1998,
publisher =	 {Springer},
month =	 {April},
pages =	 {1-12},
url =		 {http://www.aha.ru/~asarin/eq.ps.gz},
abstract =	 {We introduce quasilinear equations over timed
languages with regular coefficients. We prove that
the minimal solution of such an equation is regular
and give an algorithm to calculate this
solution. This result is used to obtain a new proof
of our Kleene-type theorem for timed
automata. Equations over timed languages can be also
considered as an alternative way of specifying these
languages}
}



@Article{Asarin:et:al00:ProcIEEE,
author =	 {E.~Asarin and O.~Bournez and T.~Dang and O.~Maler
and A.~Pnueli},
title =	 {Effective Synthesis of Switching Controllers for
Linear Systems},
journal =	 {Proceedings of the IEEE},
year =	 2000,
url =
{http://www-verimag.imag.fr/~maler/Papers/procieee.ps.gz},
note =	 {Special Issue on Hybrid Systems},
abstract =	 {In this work we suggest a novel methodology for
synthesizing switching controllers for continuous
and hybrid systems whose dynamics are defined by
linear differential equations. We formulate the
synthesis problem as finding the conditions upon
which a controller should switch the behavior of the
system from one mode'' to another in order to
avoid a set of bad states, and propose an abstract
algorithm which solves the problem by an iterative
computation of reachable states. We have implemented
a concrete version of the algorithm, which uses a
new approximation scheme for reachability analysis
of linear systems. }
}



@InProceedings{Asarin:et:al00:linear,
author =	 {E.~Asarin and O.~Bournez and T.~Dang and O.~Maler},
title =	 {Reachability Analysis of Piecewise-Linear Dynamical
Systems},
booktitle =	 {Hybrid Systems: Computation and Control},
editor =	 {B.~Krogh and N.~Lynch},
volume =	 1386,
series =	 {LNCS},
year =	 2000,
publisher =	 {Springer},
month =	 {April},
pages =	 {20-31},
url =
{http://www-verimag.imag.fr/~maler/Papers/linear.ps.gz},
abstract =	 {In this paper we describe an experimental system
called {\bf ddt} for approximating reachable states
for hybrid systems whose continuous dynamics is
defined by linear differential equations. We use an
approximation algorithm whose accumulation of errors
during the continuous evolution is much smaller than
in previously-used methods. The \ddt system can, so
far, treat non-trivial continuous systems, hybrid
systems, convex differential inclusions and
controller synthesis problems.In this paper we
discuss the problem of calculating the reachable
states of a dynamical system defined by ordinary
differential equations or inclusions. We present a
prototype system for approximating this set and
demonstrate some experimental results.}
}



@InProceedings{AsarinMaler99:optimalcontrol,
author =	 {E.~Asarin and O.~Maler},
title =	 {As Soon as Possible: Time Optimal Control for Timed
Automata},
booktitle =	 {Hybrid Systems: Computation and Control},
editor =	 {F.~Vaandrager and J.~van Schuppen},
series =	 {LNCS},
volume =	 1569,
year =	 1999,
publisher =	 {Springer},
month =	 {Mars},
pages =	 {19-30},
url =
{http://www-verimag.imag.fr/~maler/Papers/optimal.ps.gz},
abstract =	 {Time Optimal Control for Timed Automata. In this
work we tackle the following problem: given a timed
automaton, and a target set F of configurations,
restrict its transition relation in a systematic way
so that from every state, the remaining behaviors
reach F as soon as possible. This consists in
extending the controller synthesis problem for timed
automata, solved in [MPS95,AMPS98], to deal with
quantitative properties of behaviors. The problem is
formulated using the notion of a timed game
automaton, and an optimal strategy is constructed as
a fixed-point of an operator on the space of value
functions defined on state-clock configurations.}
}



@InProceedings{AsarinMalerPnueli98:discretizeddelays,
author =	 {E.~Asarin and O.~Maler and A.~Pnueli},
title =	 {On Discretization of Delays in Timed Automata and
Digital Circuits},
booktitle =	 {Proc.\ Concur'98},
editor =	 {R.~de Simone and D.~Sangiorgi},
series =	 {LNCS},
volume =	 1466,
year =	 1998,
publisher =	 {Springer},
month =	 {September},
pages =	 {470-484},
url =		 {http://www-verimag.imag.fr/~maler/Papers/disc.ps.gz},
abstract =	 { On Discretization of Delays in Timed Automata and
Digital Circuits. In this paper we solve the
following problem: "given a digital circuit composed
of gates whose real-valued delays are in an
integer-bounded interval, is there a way to
discretize time while preserving the qualitative
behavior of the circuit?" This problem is described
as open in [Brzozowski and Seger]. When
"preservation of qualitative behavior" is
interpreted in a strict sense, as having all
original sequences of events with their original
ordering we obtain the following two results: (1)
For acyclic (combinatorial) circuits whose inputs
change only once, the answer is positive: there is a
constant $\d$, depending on the maximal number of
possible events in the circuit, such that if we
restrict all events to take place at multiples of
$\d$, we still preserve qualitative behaviors. (2)
For cyclic circuits the answer is negative: a simple
circuit with three gates can demonstrate a
qualitative behavior which cannot be captured by any
discretization. Nevertheless we show that a weaker
notion of preservation, similar to that of
[Henzinger Manna and Pnueli], allows in many cases
to verify discretized circuits with $\d=1$ such that
the verification results are valid in dense time.}
}



@inproceedings{BFM99b,
author =	 {A. Bemporad and G. Ferrari-Trecate and M. Morari},
title =	 {Observability and Controllability of Piecewise
Affine and Hybrid Systems},
booktitle =	 {Proc. 38th IEEE Conf. on Decision and Control},
year =	 {1999},
url =
{http://www.aut.ee.ethz.ch/research/publications/publications.msql?action=Showdetails&project=hybrid&subproject=observ&cite=BFM99b&banner=hybrid},
abstract =	 {In this paper we prove, in a constructive way, the
equivalence between hybrid and piecewise affine
systems. By focusing our investigation on the latter
class, we show through counterexamples that
observability and controllability properties cannot
be easily deduced from those of the component linear
subsystems. Instead, we propose practical numerical
tests based on mixed-integer linear programming.}
}



@inproceedings{BGT00a,
author =	 {A. Bemporad and L. Giovanardi and F.D. Torrisi},
title =	 {Robust simulation of nonlinear electronic circuits},
booktitle =	 {Proceedings of the 8th IEEE International Workshop
on Nonlinear Dynamics of Electronic Systems},
editor =	 {G. Setti, R. Rovatti and G. Mazzini},
year =	 {2000},
month =	 may,
abstract =	 { This paper proposes robust simulation of piecewise
linear systems as a tool for the analysis of
nonlinear electronic circuits. Rather than computing
the evolution of a single trajectory, robust
simulation computes the evolution from a set of
initial conditions in the state space, for all
forcing input signals within a given class. We
describe here a tool to perform this analysis using
mathematical programming. Among various
applications, the tool allows to estimate the domain
of attraction of equilibria, and to determine if
some design specifications --- expressed themselves
in terms of reachability of subsets of the
state-space --- are met. A test of the tool on
Chua's circuit is presented.},
url =
{http://www.aut.ee.ethz.ch/research/publications/publications.msql?action=Showdetails&project=hybrid&subproject=verification&cite=BGT00a&banner=hybrid},
pages =	 {131-135}
}



@InProceedings{BHL00,
author =	 {S{\'e}bastien Bornot and Ralf Huuck and Ben Lukoschus},
title =	 {{Statische Analysetechniken f{\"u}r
speicherprogrammierbare Steuerungen}},
booktitle =	 {FBT 2000 - 10. GI/ITG-Fachgespr{\"a}ch Formale
Beschreibungstechniken'' der Gesellschaft f{\"u}r
Informatik, Informationstechnische Gesellschaft im
VDE, Fachgruppe Kommunikation und Verteilte
Systeme'', June 22/23, 2000, L{\"u}beck, Germany},
publisher =	 {Shaker-Verlag},
year =	 2000,
url =
{http://www.informatik.uni-kiel.de/~softtech/vhs/FBT2000.ps.gz},
abstract =	 {Speicherprogrammierbare Steuerungen (SPS)
unterliegen einer stark zunehmenden Verbreitung in
der Automatisierungstechnik. W{\"a}hrend diese in der
Vergangenheit meist nur zur Steuerung einfacher
Abl{\"a}ufe eingesetzt wurden, sind sie heutzutage
verantwortlich f{\"u}r die Steuerung komplexer hybrider
Systeme, sei es in der petrochemischen Industrie
oder in Kraftwerken. Daher ist eine korrekt
funktionierende Steuerungssoftware von
grunds{\"a}tzlicher Bedeutung. In diesem Vortrag wird
die Methode der statischen Analyse f{\"u}r eine
standardisierte SPS-Sprache, Anweisungsliste (AWL),
vorgestellt. Statische Analyse umfa{\ss}t Techniken, die
Laufzeitverhalten ermitteln bzw. nachweisen, ohne
den Code selbst auszuf{\"u}hren. Insbesondere die
Technik der abstrakten Interpretation spielt hier
eine wichtige Rolle. Wir werden diese Techniken mit
Bezug auf AWL vorstellen und aufzeigen, welche
statischen Analyseziele f{\"u}r AWL erreichbar
sind. Ferner gehen wir darauf ein, was statische
Analyse im Vergleich zu anderen
Verifikationstechniken leistet und wie diese in
Kombination genutzt werden k{\"o}nnen.}
}



@InProceedings{BHLL00:model,
author =	 {S{\'e}bastien Bornot and Ralf Huuck and Yassine Lakhnech
and Ben Lukoschus},
title =	 {An Abstract Model For Sequential Function Charts},
booktitle =	 {WODES 2000: 5th Workshop on Discrete Event Systems,
August 21-23, 2000, Gent, Belgium},
year =	 2000,
url =
{http://www.informatik.uni-kiel.de/~softtech/vhs/WODES2000.ps.gz},
abstract =	 {Sequential function charts (SFCs) are systems where
every step can contain other SFCs as well as state
transformations. The standard by IEC 1131-3
explicitly defines some languages for this. In this
paper we point out that the standard has many
ambiguities, and that it is crucial to have a formal
framework for the definition of SFCs. We define the
syntax and semantics of them. The semantics we give
is general enough to cope with different possible
implementations of the standard.}
}



@InProceedings{BHLL00:smv,
author =	 {S{\'e}bastien Bornot and Ralf Huuck and Yassine Lakhnech
and Ben Lukoschus},
title =	 {Verification of Sequential Function Charts using
{SMV}},
booktitle =	 {PDPTA 2000: The 2000 International Conference on
Parallel and Distributed Processing Techniques and
Applications, June 26-29, 2000, Las Vegas, Nevada,
USA},
publisher =	 {CSREA Press},
year =	 2000,
url =
{http://www.informatik.uni-kiel.de/~softtech/vhs/PDPTA2000.ps.gz},
abstract =	 {Sequential function charts (SFCs) are defined as a
modeling language in the IEC 1131-3 standard and can
be used to structure and drive programmable logic
controllers (PLCs). It includes interesting concepts
as hierarchy, history variables and priority. As the
typical application area of this language is the
control of industrial processes, it is obvious that
safety and reliability is a crucial goal for systems
using SFCs. In this work we give an abstract formal
model for SFCs and present a method to automatically
verify properties concerning the safety of such
systems using the model checking tool SMV (Symbolic
Model Verifier).}
}



@InProceedings{BHLL00:static,
author =	 {S{\'e}bastien Bornot and Ralf Huuck and Yassine Lakhnech
and Ben Lukoschus},
title =	 {Utilizing Static Analysis for Programmable Logic
Controllers},
booktitle =	 {ADPM 2000: 4th International Conference on
Automation of Mixed Processes: Hybrid Dynamic
Systems, September 18-19, 2000, Dortmund, Germany},
year =	 2000,
url =
abstract =	 {Programmable logic controllers (PLCs) occupy a big
share in automation control. However, hardly any
validation tools for their software are
available. In this work we present a lightweight
verification technique for PLC programs. In
particular, static analysis is applied to programs
written in Instruction List, a standardized language
commonly used for PLC programming. We illustrate how
these programs are annotated automatically by an
abstract interpretation algorithm which is
guaranteed to terminate and is applicable to
large-scale programs. The resulting annotations
allow static checking for possible run-time errors
and provide information about the program structure,
like existence of dead code or infinite loops, which
in combination contributes to more reliable PLC
systems.}
}



@Unpublished{BK99:cs2desc,
author =	 {Bauer, N. and Kowalewski, S.},
title =	 {Description of {VHS} Case Study 2 "{ A
Polymerization Reactor}"},
note =	 {Draft, University of Dortmund},
year =	 1999,
url =		 {http://www-verimag.imag.fr/VHS/year1/cs21b.ps}
}



@article{BM99,
author =	 {A. Bemporad and M. Morari},
title =	 {Control of Systems Integrating Logic, Dynamics, and
Constraints},
journal =	 {Automatica},
year =	 {1999},
volume =	 {35},
number =	 {3},
month =	 mar,
pages =	 {407--427},
annote =	 {\protect{\rm Special issue on hybrid systems}},
url =
{http://www.aut.ee.ethz.ch/research/publications/publications.msql?action=Showdetails&project=hybrid&subproject=mld&cite=BM99&banner=hybrid},
abstract =	 {This paper proposes a framework for modeling and
controlling systems described by interdependent
physical laws, logic rules, and operating
constraints, denoted as Mixed Logical Dynamical
(MLD) systems. These are described by linear dynamic
equations subject to linear inequalities involving
real and integer variables. MLD systems include
constrained linear systems, finite state machines,
some classes of discrete event systems, and
nonlinear systems which can be approximated by
piecewise linear functions. A predictive control
scheme is proposed which is able to stabilize MLD
systems on desired reference trajectories while
fulfilling operating constraints, and possibly take
into account previous qualitative knowledge in the
form of heuristic rules. Due to the presence of
integer variables, the resulting on-line
optimization procedures are solved through Mixed
Integer Quadratic Programming (MIQP), for which
efficient solvers have been recently developed. Some
examples and a simulation case study on a complex
gas supply system are reported. }
}



@InProceedings{BMG99:orthogonalpolyhedra,
author =	 {O.~Bournez and O.~Maler and A.~Pnueli},
title =	 {Orthogonal Polyhedra: Representation and
Computation},
booktitle =	 { Hybrid Systems: Computation and Control},
editor =	 {F.~Vaandrager and J.~van Schuppen},
series =	 {LNCS},
volume =	 1569,
year =	 1999,
publisher =	 {Springer},
month =	 {Mars},
pages =	 {46-60},
url =
{http://www-verimag.imag.fr/~maler/Papers/griddy.ps.gz},
abstract =	 {Orthogonal Polyhedra: Representation and
Computation. In this paper we investigate orthogonal
polyhedra, i.e. polyhedra which are finite unions of
full-dimensional hyper-rectangles. We define
representation schemes for these polyhedra based on
their vertices, and show that these compact
representation schemes are canonical for all (convex
and non-convex) polyhedra in any dimension. We then
develop efficient algorithms for membership,
face-detection and Boolean operations for these
representations.}
}



@InProceedings{BMT99,
author =	 {M.~Bozga and O.~Maler and S.~Tripakis},
title =	 {Efficient Verification of Timed Automata using Dense
and Disrete Time Semantics},
booktitle =	 {Proc.\ CHARME'99},
editor =	 {T.~Kropf and L.~Pierre},
volume =	 {1703},
series =	 {LNCS},
year =	 1999,
publisher =	 {Springer},
month =	 {September},
pages =	 {125--141},
url =
{http://www-verimag.imag.fr/~maler/Papers/stari.ps.gz},
abstract =	 {In this paper we argue that the semantic issues of
{\em discrete} vs.\ {\em dense} time should be
separated as much as possible from the pragmatics of
state-space representation. Contrary to some
misconceptions, the discrete semantics is not
inherently bound to use state-explosive techniques
any more than the dense one. In fact, discrete timed
automata can be analyzed using any representation
scheme (such as DBM) used for dense time, and in
addition can benefit from enumerative and symbolic
techniques (such as BDDs) which are not naturally
applicable to dense time. DBMs, on the other hand,
can still be used more efficiently by taking into
account the {\em activity} of clocks, to eliminate
redundancy. To support these claims we report
experimental results obtained using an extension of
Kronos with BDDs and variable-dimension DBMs where
we verified the asynchronous chip STARI, a FIFO
buffer which provides for skew-tolerant
communication between two synchronous systems. Using
discrete time and BDDs we were able to prove
correctness of a STARI implementation with 18 stages
(55 clocks), better than what has been achieved
using other techniques. The verification results
carry over to the dense semantics. Using
variable-dimension DBMs we have managed to verify
STARI for up to 8 stages (27 clocks). In fact, our
analysis shows that at most one third of the clocks
are active at any reachable state, and about one
fourth of the clocks are active in 90\% of the
reachable states. These results explain perhaps the
reduction achieved using BDDs.}
}



@Unpublished{BMW99:cs1plc,
author =	 {Angelika Mader and Hanno Wupper and Nanette Bauer},
title =	 {Design of a {PLC} Program for {VHS} Case Study 1},
note =	 {draft},
url =		 {http://www-verimag.imag.fr/VHS/year1/cs11h.ps},
year =	 1999,
abstract =	 {Our goal of this paper is twofold. First, we tried
to derive a control program for VHS case study 1 in
a systematic way that also gives indication of the
correctness of the program. Second, we are
interested in a method that supports the control
program design. This report presents our first
results and conclusions with respect to a simple
specification formalism for hard real-time problems,
a specification method allowing to derive the
specification of a control program in a systematic
way from the properties of the plant to be
controlled, the application of the specification
method to the case study, the formal verification of
the specification of a program for single batch
operation with respect to the specification of the
overall plant using PVS, a control program for
single batch operation written in SFC, an informal
verification of the specification of the program for
multiple batch operation with respect to the
specification of the overall plant using PVS,
extensions in the functionality of the control
program in an informal way.}
}



@TECHREPORT{BT00,
author =	 {A. Bemporad and F.D. Torrisi},
year =	 2000,
title =	 {Inner and Outer Approximation of Polytopes Using
Hyper-Rectangles},
number =	 {AUT00-02},
institution =	 {Automatic Control Lab, ETH Zurich},
abstract =	 {In this note we consider the following problem in
polyhedral computation: find two sets of
hyper-rectangles which inner- and outer-approximate
a given polytope in $R^d$. We assume that the
polytope is given by halfspaces (H-polytopes). As a
by-product, the algorithm provides an approximate
computation of the volume and of orthogonal
projections. },
url =
{http://www.aut.ee.ethz.ch/research/publications/publications.msql?action=Showdetails&project=hybrid&subproject=verification&cite=BT00&banner=hybrid}
}



@inproceedings{BTM00,
author =	 {A. Bemporad and F.D. Torrisi and M. Morari},
title =	 {Optimization-Based Verification and Stability
Characterization of Piecewise Affine and Hybrid
Systems},
booktitle =	 {Hybrid Systems: Computation and Control},
editor =	 {B. Krogh and N. Lynch},
series =	 {Lecture Notes in Computer Science},
volume =	 {1790},
publisher =	 {Springer Verlag},
year =	 {2000},
url =
{http://www.aut.ee.ethz.ch/research/publications/publications.msql?action=Showdetails&project=hybrid&subproject=verification&cite=BTM00&banner=hybrid},
abstract =	 {In this paper, we formulate the problem of
characterizing the stability of a piecewise affine
(PWA) system as a verification problem. The basic
idea is to take the whole $R^n$ as the set of
initial conditions, and check that all the
trajectories go to the origin. More precisely, we
test for semi-global stability by restricting the
set of initial conditions to an (arbitrarily large)
bounded set $XX(0)$, and label as asymptotically
stable in $T$ steps'' the trajectories that enter an
invariant set around the origin within a finite time
$T$, or as unstable in $T$ steps'' the
trajectories which enter a (very large) set
$XXinst$. Subsets of $XX(0)$ leading to none of the
two previous cases are labeled as not classifiable
in $T$ steps''. The domain of asymptotical stability
in $T$ steps is a subset of the domain of attraction
of an equilibrium point, and has the practical
meaning of collecting initial conditions from which
the settling time of the system is smaller than
$T$. In addition, it can be computed algorithmically
in finite time. Such an algorithm requires the
computation of reach sets, in a similar fashion to
what has been proposed for verification of hybrid
systems. In this paper we present a substantial
extension of the verification algorithm presented
in~(Bemporad and Morari, 1999, LNCS 1569) for
stability characterization of PWA systems, which is
based on linear and mixed-integer linear
programming. As a result, given a set of initial
conditions we are able to determine its partition
into subsets of trajectories which are either
asymptotic stable, or unstable, or not classifiable
in $T$ steps. },
pages =	 {45--58},
}



@techreport{BTM00b,
author =	 {A. Bemporad and F.D. Torrisi and M. Morari},
title =	 {Verification of Mixed Logical Dynamical Models ---
The Batch Evaporator Process Benchmark},
institution =	 {Automatic Control Laboratory},
year =	 {2000},
number =	 {AUT00-04},
month =	 feb,
note =	 {\texttt{http://control.ethz.ch/}},
abstract =	 {In this paper we show how the MLD modeling framework
introduced in~\cite{BM99} and the reachability
analysis algorithm presented
in~\cite{BeMo99-2,BTM00} can be successfully used to
solve the batch evaporator benchmark verification
problem~\cite{Kow98}. MLD models describe hybrid
systems where discrete-time linear dynamic
equations, logic rules, and automata interact. The
reachability analysis algorithm is based on linear
and mixed-integer linear programming. After
reviewing MLD models and the algorithm, we detail
the modeling of the batch evaporator benchmark
process and its verification in order to illustrate
the versatility of the analysis tool.},
url =
{http://www.aut.ee.ethz.ch/research/publications/publications.msql?action=Showdetails&project=hybrid&subproject=verification&cite=BTM00b&banner=hybrid},
annote =	 {submitted EJC - Special Issue VHS},
}



@techreport{BVFKL99,
author =	 "Bodentien, Nicky O. and Vestergaard, Jacob and
Friis, Jakob and Kristoffersen, K{\aa}re J. and Larsen,
Kim G.",
title =	 "Verification of State/Event Systems by Quotienting",
institution =	 {BRICS},
year =	 1999,
number =	 "RS-99-41",
month =	 dec,
note =	 "17~pp. Presented at {\em Nordic Workshop in
Programming Theory}, Uppsala, Sweden, October 6--8,
1999",
abstract =	 "A rather new approach towards compositional
verification of concurrent systems is the quotient
technique, where components are gradually removed
from the concurrent system while transforming the
specification accordingly. When the intermediate
specifications can be kept small, the state
explosion problem is avoided and there are already
promising experimental results for systems with an
interleaving semantics, including real-time
systems. This paper extends the quotienting approach
to deal with a synchronous framework in the shape of
state/event systems with acyclic dependencies. A
state/event system is a concurrent system with a set
of interdependent components operating synchronously
according to stimuli provided by an environment. We
introduce Left Restricting state/event systems as a
key notion for state/event systems with acyclic
dependencies. Two families of modal logics,
$\mathcal{L}$ and $\mathcal{M}$, specifically
designed for expressing reachability properties of
dependency closed and not dependency closed
subsystems are introduced. Two quotient
constructions for moving components from dependency
closed and not dependency closed subsystems into the
specification are presented and their correctness
are justified in a formal proof. Furthermore,
heuristics for minimizing formulae are proposed and
the techniques are demonstrated on a Duplo train
example",
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/BVFKL99.ps.gz}
}



@Unpublished{Bau00:cs7descr,
author =	 {Nanette Bauer},
title =	 {A demonstration plant for the control and scheduling
of multi-product batch operations},
note =	 {VHS Case Study 7},
url =		 {http://www-verimag.imag.fr/VHS/CS7/cs7descr.ps},
year =	 2000,
abstract =	 {In this report a new laboratory plant which was
designed and built at the Process Control Laboratory
of the University of Dortmund is presented as a case
example. The purpose of the plant is to serve as a
test-bed and a demonstration medium for control and
scheduling methods for multi product batch plants. A
scheduling problem is proposed and the control
architecture which has been designed integrating
both control and scheduling aspects is described.}
}



@Unpublished{Bau99:cs2smv,
author =	 {Bauer, N.},
title =	 {Verification of {VHS} Case Study 2 using {SMV}},
note =	 {Draft, University of Dortmund},
url =		 {http://www-verimag.imag.fr/VHS/year1/cs21c.ps},
year =	 1999
}



@InProceedings{BeHuVa00,
author =	 {Gerd Behrmann and Thomas Hune and Frits Vaandrager},
title =	 {Distributed Timed Model Checking - {H}ow the Search
Order Matters},
booktitle =	 {Proc. of 12th International Conference on Computer
Aided Verification},
year =	 2000,
month =	 {Juli},
series =	 {Lecture Notes in Computer Science},
publisher =	 {Springer-Verlag},
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/bhv-cav2000.ps.gz}
}



@incollection{BeMo99-2,
title =	 {Verification of hybrid systems via mathematical
programming},
booktitle =	 {Hybrid Systems: Computation and Control},
editor =	 {F.W. Vaandrager and J.H. van Schuppen},
series =	 {Lecture Notes in Computer Science},
volume =	 {1569},
publisher =	 {Springer Verlag},
year =	 {1999},
abstract =	 {This paper proposes a novel approach to the
verification of hybrid systems based on linear and
mixed-integer linear programming. Models are
described using the Mixed Logical Dynamical (MLD)
formalism introduced in (Bemporad, Morari 1999). The
proposed technique is demonstrated on a verification
case study for an automotive suspension system. },
url =
{http://www.aut.ee.ethz.ch/research/publications/publications.msql?action=Showdetails&project=hybrid&subproject=verification&cite=BeMo99-2&banner=hybrid},
pages =	 {31--45}
}



@InProceedings{BoBoSt1:98,
author =	 {R.K. Boel and B. Bordbar and G. Stremersch},
title =	 {A min-plus polynomial approach to forbidden state
control for general {Petri} nets},
booktitle =	 {Proceedings of the 4th International Workshop on
Discrete Event Systems},
organization = {IEE},
month =	 {August},
pages =	 {79--84},
year =	 {1998},
abstract =	 {This paper treats feedback control design for
discrete event systems, modeled as Petri nets, with
avoidance of forbidden states as specification of
the control goal. It has been shown before that for
calculating maximally permissive feedback controls
attention can be limited to the marking of a subnet,
the influencing net. We first show that the
influencing net can be described algorithmically
using min-plus algebra. Next we introduce a general
approach for calculating state feedback controls by
decomposing the set of places and the set of
transitions in the uncontrolled net in a number of
layers. These layers are used to construct a
min-plus polynomial which has to be maximized to
obtain the maximal value of the expressions
specifying the control goal. An example shows that
in many interesting cases it is possible to
eliminate most of the variables, allowing efficient
control design for general Petri net models.}
}



@InProceedings{BoBoSt2:98,
author =	 {R.K. Boel and B. Bordbar and G. Stremersch},
title =	 {Controlled timed {Petri} nets: equivalence
relations, model reduction},
booktitle =	 {Proceedings of the IEEE International Conference on
Systems, Man and Cybernetics},
year =	 {1998},
organization = {IEEE},
url =
{http://www-verimag.imag.fr/VHS/resources/BBS98.ps.gz},
abstract =	 {This paper discusses controlled timed Petri net
models for the formal synthesis of supervisory
controllers for real time discrete event systems
(e.g.\ communication protocols, supervisors for
FMSs, control of batch processes). We extend the
standard Petri net formalism with firing delays
between the time a transition becomes state enabled,
and the time it is executed. These firing delays are
partly controllable between lower and upper
bounds. The goal is to guarantee that certain
forbidden distributions of tokens will never
occur. For this purpose we define the influencing
net corresponding to forbidden sets. Deciding
whether a maximally permissive controller exists,
and if yes, constructing such a controller, requires
solving large sets of linear inequalities over
firing times in this influencing net. This is
generally a very large set. Hence we study some
equivalence relations between different subnets of a
timed Petri net. An example shows that replacing a
subnet by a simpler equivalent subnet can
significantly reduce the size of the sets of
inequalities to be solved.}
}



@InProceedings{BoMo:00,
author =	 {R.K. Boel and F. J. Montoya},
title =	 {Modular Synthesis of efficient schedules in a timed
discrete event plant},
booktitle =	 {submitted for CDC2000},
year =	 2000,
url =
{http://www-verimag.imag.fr/VHS/resources/BoMo00.ps.gz},
abstract =	 {This paper treats optimal scheduling in large timed
discrete event systems as a supervisory control
problem. This paper considers a case study where a
schedule must be synthesized which completes a
sequence of tasks in the shortest possible time,
while satisfying all the constraints in the model,
and satisfying some hard outside constraints. The
paper emphasizes the importance of describing the
plant via a graph of interacting modules, Each
module can be represented using a different
mathematical formalisms. An algorithm is proposed
for efficiently finding an optimal schedule by first
finding an optimal schedule in each module
separately, for the largest subset of modules which
form an acyclic graph.}
}



@Unpublished{BoSt99:cs5,
author =	 {Ren{\'e} Boel and Geert Stremersch},
title =	 {{VHS} Case Study 5: modelling and verification of
scheduling for steel plant at {SIDMAR}},
note =	 {draft},
url =		 {http://www-verimag.imag.fr/VHS/CS5/tpnsidm2.ps.gz},
year =	 1999
}



@Unpublished{BoSt99:cs5appendix,
author =	 {Ren{\'e} Boel and Geert Stremersch},
title =	 {{VHS} Case Study 5: Timed {Petri} net model of steel
plant at {SIDMAR}},
note =	 {draft},
url =
{http://www-verimag.imag.fr/VHS/CS5/tpnappendix.ps.gz},
crossref =	 {BoSt99:cs5},
year =	 1999
}



@Unpublished{BoSt99:cs5tpnsemantics,
author =	 {Ren{\'e} Boel and Geert Stremersch},
title =	 {Semantics of Timed {Petri} nets},
note =	 {draft},
url =		 {http://www-verimag.imag.fr/VHS/CS5/tpnseman.ps.gz},
crossref =	 {BoSt99:cs5},
year =	 1999
}



@InCollection{BoSt:98,
author =	 {R.K. Boel and G. Stremersch},
title =	 {Forbidden state control synthesis for timed {Petri}
net models},
booktitle =	 {Open Problems in Mathematical Systems and Control
Theory},
pages =	 {61--66},
publisher =	 {Springer-Verlag London},
year =	 {1998},
editor =	 {V.D. Blondel, E.D. Sontag, M. Vidyasagar and
J.C. Willems},
url =		 {http://www-verimag.imag.fr/VHS/resources/BS98.ps.gz},
abstract =	 {Design of controllers for large, computer controlled
plants often involves system models exhibiting
dynamics in both continuous and discrete state
space. This note uses controlled timed Petri nets
model for such hybrid systems. The evolution of a
timed Petri net is described by the transfer of
tokens in between places via execution of
transitions. Real time is introduced by modelling
the time interval required for the execution of
transitions. Control is implemented by delaying some
of the transitions. The control goal is that the
state never reaches a set of forbidden states. This
note discusses the question of extending the known,
efficient algorithms obtained for untimed Petri nets
to the design of maximally permissive feedback
controls for forbidden state avoidance. The main
difficulties in this extension are: the definition
of the equivalent notion corresponding to the
influencing net for untimed Petri nets; and the
effects of forced transitions.}
}



@Unpublished{Boel98:cs5,
author =	 {Boel, R.},
title =	 {Description of the Sidmar steel plant},
note =	 {Draft, University of Ghent},
year =	 1998
}



@InProceedings{Boel:00,
author =	 {R.K. Boel},
title =	 {Automatic Synthesis of Schedules in a timed discrete
event plant},
year =	 2000,
url =		 {http://www-verimag.imag.fr/VHS/resources/Bo00.ps.gz},
abstract =	 { This paper discusses modular synthesis of optimal
schedules for large plants. By distinguishing
foreground and background events, and by decomposing
the plant model in separate modules which have
physical meaning it is possible to achieve synthesis
of an optimal schedule without having to search
through the whole state space. It is assumed that
all scheduling decisions which explicitly determine
the cost to be minimized belong to the foreground
modules. A schedule is determined for the foreground
modules together. This schedule imposes certain
constraints on the background modules, and a
verification tool is used in order to check whether
the background modules can satisfy thiese
constraints. For some models, such as a steel plant,
the graph of foregroud modules is acyclic, and
optimisation can be done via backward recursion from
last module moving up through all predecessor
modules. For other models, such an urban traffic
model, the foreground modules are interconnected in
a cyclic graph, and iteration is necessary in order
to find an optimal schedule in the foreground
model.}
}



@inproceedings{BornotGoesslerSifakis2000,
author =	 {S. Bornot and G. G{\"o}{\ss}ler and J. Sifakis},
title =	 "On the Construction of Live Timed Systems",
booktitle =	 "TACAS 2000 proceedings",
pages =	 {109-126},
volume =	 1785,
year =	 2000,
series =	 {LNCS},
publisher =	 {Springer-Verlag},
abstract =	 {A method that allows to guarantee liveness by
construction of a class of timed systems is
presented. The method is based on the use of a set
of structural properties which can be checked
locally at low cost. Sufficient conditions for
liveness preservation by parallel composition and
priority choice operators are provided. The latter
allow to restrict a system's behavior according to a
given priority order on its actions. Several
examples illustrating the use of the results are
presented, in particular for the construction of
live controllers.},
url =
{http://www-verimag.imag.fr/VHS/resources/goe2000.ps.gz}
}



@InProceedings{BournezMaler00:tpoly,
author =	 {O.~Bournez and O.~Maler},
title =	 {On the Representation of Timed Polyhedra},
booktitle =	 {Proc.\ ICALP'00},
series =	 {LNCS},
year =	 2000,
publisher =	 {Springer},
month =	 {July},
url =
{http://www-verimag.imag.fr/~maler/Papers/tpoly.ps.gz},
abstract =	 {In this paper we argue that the semantic issues of
{\em discrete} vs.\ {\em dense} time should be
separated as much as possible from the pragmatics of
state-space representation. Contrary to some
misconceptions, the discrete semantics is not
inherently bound to use state-explosive techniques
any more than the dense one. In fact, discrete timed
automata can be analyzed using any representation
scheme (such as DBM) used for dense time, and {\em
in addition} can benefit from enumerative and
symbolic techniques (such as BDDs) which are not
naturally applicable to dense time. DBMs, on the
other hand, can still be used more efficiently by
taking into account the {\em activity} of clocks, to
eliminate redundancy. To support these claims we
report experimental results obtained using an
extension of Kronos with BDDs and variable-dimension
DBMs where we verified the asynchronous chip STARI,
a FIFO buffer which provides for skew-tolerant
communication between two synchronous systems. Using
discrete time and BDDs we were able to prove
correctness of a STARI implementation with 18 stages
(55 clocks), better than what has been achieved
using other techniques. The verification results
carry over to the dense semantics. Using
variable-dimension DBMs we have managed to verify
STARI for up to 8 stages (27 clocks). In fact, our
analysis shows that at most one third of the clocks
are active at any reachable state, and about one
fourth of the clocks are active in 90\% of the
reachable states. }
}



@InProceedings{BozgaMaler99:PDG,
author =	 {M.~Bozga and O.~Maler},
title =	 { On the Representation of Probabilities over
Structured Domains},
booktitle =	 {Proc.\ CAV'99},
editor =	 { N.~Halbwachs and D.~Peled},
volume =	 {1633},
series =	 {LNCS},
year =	 1999,
publisher =	 {Springer},
month =	 {June},
pages =	 {261-273},
url =		 {http://www-verimag.imag.fr/~maler/Papers/pdg.ps.gz},
abstract =	 {In this paper we extend one of the main tools used
in verification of discrete systems, namely Binary
Decision Diagrams (BDD), to treat probabilistic
transition systems. We show how probabilistic
vectors and matrices can be represented canonically
and succinctly using probabilistic trees and graphs,
and how simulation of large-scale probabilistic
systems can be performed. We consider this work as
an important contribution of the verification
community to numerous domains which need to
manipulate very large matrices.}
}



@InProceedings{BozgaMaler99:probabilities,
author =	 {M.~Bozga and O.~Maler},
title =	 {On the Representation of Probabilities over
Structured Domains},
booktitle =	 {Proc.\ CAV'99},
editor =	 { N.\ Halbwachs and D.\ Peled},
volume =	 {1633},
series =	 {LNCS},
year =	 1999,
publisher =	 {Springer},
month =	 {Jule},
pages =	 {261--273},
url =		 {http://www-verimag.imag.fr/~maler/Papers/pdg.ps.gz},
abstract =	 {In this paper we extend one of the main tools used
in verification of discrete systems, namely Binary
Decision Diagrams (BDD), to treat probabilistic
transition systems. We show how probabilistic
vectors and matrices can be represented canonically
and succinctly using probabilistic trees and graphs,
and how simulation of large-scale probabilistic
systems can be performed. We consider this work as
an important contribution of the verification
community to numerous domains which need to
manipulate very large matrices.}
}



author =	 {M.~Bozga and O.~Maler and S.~Tripakis},
title =	 {Efficient Verification of Timed Automata using Dense
and Discrete Time Semantics},
booktitle =	 {Proc.\ Charme'99},
editor =	 {L.~Pierre and T.~Kropf},
volume =	 1703,
series =	 {LNCS},
year =	 1999,
publisher =	 {Springer},
month =	 {September},
pages =	 {125-141},
url =
{http://www-verimag.imag.fr/~maler/Papers/stari.ps.gz},
abstract =	 {In this paper we investigate {\it timed polyhedra},
i.e.\ polyhedra which are finite unions of full
dimensional simplices of a special kind. Such
polyhedra form the basis of timing analysis and in
particular of verification tools based on timed
automata. We define a representation scheme for
these polyhedra based on their extreme vertices, and
show that this compact representation scheme is
canonical for all ({\em convex and non-convex})
polyhedra in {\em any} dimension. We then develop
relatively efficient algorithms for membership,
boolean operations, projection and passage of time
for this representation.}
}



@Unpublished{CaLa00,
author =	 {Franck Cassez and Kim G. Larsen},
title =	 {The Impressive Power of Stopwatches},
note =	 {To appear in Proceedings of CONCUR'2000},
year =	 2000,
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/CaLa00.ps.gz}
}



@inproceedings{DFMV98a,
author =	 {H. Dierks and A. Fehnker and A. Mader and
F.W. Vaandrager},
title =	 {Operational and logical semantics for polling
real-time systems},
booktitle =	 {Proceedings of the Fifth International Symposium on
Formal Techniques in Real-Time and Fault-Tolerant
Systems (FTRTFT'98), Lyngby, Denmark},
editor =	 {A.P. Ravn and H. Rischel},
series =	 {LNCS},
volume =	 1486,
publisher =	 {Springer},
year =	 1998,
pages =	 {29--40},
note =	 {Extended version available as Report CSI-R9813,
Computing Science Institute, University of Nijmegen,
April 1998},
url =
{http://www.cs.kun.nl/csi/reports/info/CSI-R9813.html},
abstract =	 { PLC-Automata are a class of real-time automata
suitable to describe the behaviour of polling
real-time systems. PLC-Automata can be compiled to
source code for PLCs, a hardware widely used in
industry to control processes. Also, PLC-Automata
have been equipped with a logical and operational
semantics, using Duration Calculus (DC) and Timed
Automata (TA), respectively. The three main results
of this paper are: (1) A simplified operational
semantics. (2) A minor extension of the logical
semantics, and a proof that this semantics is {\em
complete} relative to our operational
semantics. This means that if an observable
satisfies all formulas of the DC semantics, then it
can also be generated by the TA semantics. (3) A
proof that the logical semantics is {\em sound}
relative to our operational semantics. This means
that each observable that is accepted by the TA
semantics constitutes a model for all formulas of
the DC semantics. }
}



@Article{DK00comparison,
author =	 {G. D{\"u}nnebier and K.-U. Klatt},
title =	 {Modeling and Simulation of Nonlinear Chromatographic
Separation Processes: A Comparison of Different
Modeling Approaches},
journal =	 {Chem. Engng. Sci.},
year =	 2000,
volume =	 55,
pages =	 {373--380},
url =		 {http://www-verimag.imag.fr/VHS/CS3/ces99.pdf}
}



@Article{DWK98:movingbed,
author =	 {G. D{\"u}nnebier and I. Weirich and K.-U. Klatt},
title =	 {Computationally efficient dynamic modeling and
simulation of simulated moving bed chromatographic
processes with linear isotherms},
journal =	 {Chem. Engng. Sci.},
year =	 1998,
volume =	 53,
number =	 14,
pages =	 {2537-2546},
url =		 {http://www-verimag.imag.fr/VHS/CS3/CES98.pdf}
}



@Unpublished{DaWa00,
author =	 {Alexandre David and Wang Yi},
title =	 {Debugging a Commercial Field Bus Protocol},
note =	 {To appear in the proceedings of the 12th Euromicro
Conference On ReaL-Time Systems.},
year =	 2000,
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/DaWa00.ps.gz}
}



@InProceedings{DangMaler98:facelifting,
author =	 {T.~Dang and O.~Maler},
title =	 {Reachability Analysis via Face Lifting},
booktitle =	 {Hybrid Systems: Computation and Control},
editor =	 {T.A.~Henzinger and S.~Sastry},
volume =	 1386,
series =	 {LNCS},
year =	 1998,
publisher =	 {Springer},
month =	 {April},
pages =	 {96-109},
url =
{http://www-verimag.imag.fr/~maler/Papers/facelift.ps.gz},
abstract =	 {In this paper we discuss the problem of calculating
the reachable states of a dynamical system defined
by ordinary differential equations or inclusions. We
present a prototype system for approximating this
set and demonstrate some experimental results.}
}



title =	 {A switched continuous model of {VHS} Case Study 1},
note =	 {Draft, University of Dortmund},
month =	 {feb},
url =		 {http://www-verimag.imag.fr/VHS/year1/cs11c.ps},
year =	 1999
}



@Unpublished{EDB99:dcs,
author =	 {Sebastian Engell and Andre Deparade and Nanette
Bauer},
title =	 {State of the art and needs in the imprementation of
process control software in {DCS}},
note =	 {VHS deliverable in Workpackage IP.1},
month =	 {March},
year =	 1999,
url =		 {http://www-verimag.imag.fr/VHS/IP/uhde.ps}
}



@Proceedings{Embedded98,
title =	 {Lectures on Embedded Systems},
booktitle =	 {Lectures on Embedded Systems},
editor =	 {G. Rozenberg and F.W. Vaandrager},
year =	 1998,
month =	 oct,
series =	 {LNCS},
volume =	 1494,
publisher =	 {Springer},
crossrefonly = 1
}



@TechReport{Fehnker00:BandB,
author =	 {Ansgar Fehnker},
title =	 {Bounding and heuristics in forward reachability
algorithms},
institution =	 {Computing Science Institute Nijmegen},
year =	 2000,
month =	 feb,
number =	 {CSI-R0002},
url =
{http://www.cs.kun.nl/csi/reports/info/CSI-R0002.html},
abstract =	 {Recently timed automata models have been used to
solve realistic scheduling problems. In this paper
we want to establish the relation between timed
automata and job shop scheduling problems. The timed
automata models of the scheduling problems can serve
as input for a forward reachability checker. In
contrast to job shop algorithms the forward
reachability algorithms will usually not yield an
optimal solution. There are also only few ways to
direct the exploration of the state space. Starting
from job shop problem we will describe how forward
reachability can be equipped with two concepts from
branch and bound methods: heuristics and
bounding. This extended algorithm is then applicable
to all kinds of timed automata models.}
}



@TechReport{Fehnker99:cs5,
author =	 {Ansgar Fehnker},
title =	 {Scheduling a Steel Plant with Timed Automata},
institution =	 {Computing Science Institute Nijmegen},
year =	 1999,
number =	 {CSI-R9910},
url =
{http://www.cs.kun.nl/~ansgar/vhs/sidmar/poging.ps.gz}
}

@InProceedings {Fehnker99:rtcsa,
author =	 {Ansgar Fehnker},
title =	 {Scheduling a Steel Plant with Timed Automata},
booktitle =	 {Proceedings of the 6th International Conference on
Real-Time Computing Systems and Applications
(RTCSA99)},
organization = {IEEE Computer Society},
pages =	 {280-286},
year =	 {1999},
url =		 {http://www.cs.kun.nl/~ansgar/vhs/sidmar/stuk.ps.gz},
abstract =	 {Scheduling in an environment with constraints of
many different types is known to be a hard
problem. We tackle this problem for a integrated
steel plant in Ghent, Belgium, using Uppaal, a model
checker for networks of timed automata. We show how
to translate schedulability to reachability,
enabling us to use Uppaal's model checking
algorithms.}
}



@unpublished{FeyJHvS99:cs4r1,
author =	 {Jeroen J.H. Fey and Jan H. van Schuppen},
title =	 {{VHS} Case Study 4 - Verification and control of a
juice processing plant},
note =	 {draft},
year =	 {1999},
url =
{http://www.cwi.nl/~schuppen/projects/vhs/cs4r1figs.ps.gz},
class =	 {m93s89} ,
abstact =	 {The aim of Case Study 4 of Project VHS is to
investige the applicability of algorithms and theory
for hybrid systems to a juice processing plant. This
first report contains a brief description of the
plant, several schedules of the operations of juice
processing, and constraints on the schedules. For
the verification problem of the schedule an outline
is presented. For the control problem a first
problem formulation is presented.}
}



@unpublished{FeyJHvS99:cs4r2,
author =	 {Jeroen J.H. Fey and Jan H. van Schuppen},
title =	 {{VHS} Case Study 4 - Modeling and control of a juice
processing plant},
note =	 {draft},
year =	 {1999},
url =		 {http://www-verimag.imag.fr/VHS/CS4/dcs42.ps.gz},
class =	 {m93s89}
,
}



@Article{FlTh00:modularhybrid,
author =	 {Luc Thevenon and Jean-Marie Flaus},
title =	 {Modular Representation of complex hybrid systems:
Application to the simulation of batch processes},
journal =	 {Accepted for publication in the Journal of
Simulation Practice},
year =	 2000,
url =
{http://www-verimag.imag.fr/VHS/resources/FlTh00simpra.pdf}
}



@InProceedings{Flaus98:discretesupervisorsynth,
author =	 {Jean-Marie Flaus},
title =	 {Discrete supervisor synthesis for a class of
continuous systems},
booktitle =	 {CDC'98},
year =	 1998,
publisher =	 {IEEE},
month =	 {December},
url =
{http://www-verimag.imag.fr/VHS/resources/Flaus98.ps.gz}
}



@Unpublished{HLP99:cs5,
author =	 {Thomas Hune and Kim G.~Larsen and Paul Pettersson},
title =	 {Guided Synthesis of Control Programs using {UPPAAL}
for {VHS} Case Study 5},
note =	 {VHS deliverable in Workpackage CS.1.1},
year =	 1999,
url =		 {http://www.cs.auc.dk/research/FS/VHS/hlp99.ps.gz},
abstract =	 {In this paper we address the problem of synthesizing
control programs for a physical plant, such as the
steel production plant of SIDMAR, from a timed
automata model of the plant. We present a model of
the plant that faithfully reflects the level of
abstraction required for synthesizing control
programs. As this very detailed model quickly
becomes too complicated for automatic synthesis, we
also present a guided model. We present a general
way of adding guidance to a model by augmenting the
model with additional guide variables and decorating
the transitions with extra guards. We have
successfully applied the method to our models,
making automatic synthesis feasible for larger
models.}
}



@inproceedings{HuLaPe00,
author =	 {Thomas Hune and Kim G. Larsen and Paul Pettersson},
title =	 {Guided Synthesis of Control Programs Using {Uppaal}},
booktitle =	 {Proc.\ of the IEEE ICDCS International Workshop on
Distributed Systems Verification and Validation},
pages =	 {E15--E22},
editor =	 {Ten H. Lai},
year =	 2000,
month =	 Apr,
publisher =	 {IEEE Computer Society Press},
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/hlp-dsvv00.ps.gz}
}



@inproceedings{HuSa00C,
author =	 "Hune, Thomas S. and Sandholm, Anders B.",
title =	 "A Case Study on using Automata in Control Synthesis",
booktitle =	 {Fundamental Approaches to Software Engineering
(FASE)},
year =	 2000,
pages =	 "349--362",
month =	 mar,
series =	 {LNCS},
abstract =	 "We study a method for synthesizing control
programs. The method merges an existing control
program with a control automaton. We have used
monadic second order logic over strings to specify
the control automata. Specifications are translated
into automata by the Mona tool. This yields a new
control program restricting the behavior of the old
control program such that the specifications are
satisfied. The method is presented through a
concrete example.",
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/HuSa00.ps.gz}
}



@TechReport{Huuck99a,
author =	 {Ralf Huuck},
title =	 {Transformation of Timed Condition/Event Systems into
Timed Automata: An Approach to Automatic
Verification},
institution =	 {Christian-Albrechts-Universit{\"a}t zu Kiel},
year =	 1999,
number =	 {(number to be assigned)},
url =		 {http://www-verimag.imag.fr/VHS/year1/cs11j.ps}
}



@TechReport{Huuck99b,
author =	 {Ralf Huuck},
title =	 {Verifying Timing Aspects of {VHS} Case Study 1},
institution =	 {Christian-Albrechts-Universit{\"a}t zu Kiel},
year =	 1999,
number =	 {(number to be assigned)},
url =		 {http://www-verimag.imag.fr/VHS/year1/cs11i.ps},
abstract =	 {This paper deals with an exception handling for Case
Study 1. A number of orthogonal timing constraints
define a challenging control problem. We examine
this one using timed automata for modeling, and
Kronos and HyTech for model-checking. Additionally,
we approach it using timed condition/event systems
as the basic model and analyze these ones by
transforming them automatically into Kronos code and
checking them on this level.}
}



@proceedings{Hybrid99,
title =	 {Proceedings Second International Workshop on Hybrid
Systems: Computation and Control (HSCC'99), {\rm
Berg en Dal, The Netherlands}},
booktitle =	 {Proceedings Second International Workshop on Hybrid
Systems: Computation and Control (HSCC'99), {\rm
Berg en Dal, The Netherlands}},
year =	 1999,
month =	 mar,
editor =	 {F.W. Vaandrager and J.H. van Schuppen},
crossrefonly = 1,
key =		 {HSCC'99},
series =	 {LNCS},
volume =	 1569,
publisher =	 {Springer}
}



@unpublished{IKLLMMPT00,
author =	 {Iversen, Torsten K. and Kristoffersen, K{\aa}re J. and
Larsen, Kim G. and Laursen, Morten and Madsen, Rune
G. and Mortensen, Steffen K. and Pettersson, Paul
and Thomasen, Chris B.},
title =	 {Model-Checking Real-Time Control Programs ---
{V}erifying {LEGO} Mindstorms Systems Using
{Uppaal}},
year =	 2000,
note =	 {To appear in ECRTS'2000.},
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/ikllmmpt-ecrts00.ps.gz}
}



@TechReport{ILOGeval,
author =	 {Sidmar},
title =	 {Evaluation Report on ILOG Scheduler.},
institution =	 {Systems and Modellling Division, Sidmar.},
year =	 1999,
type =	 {internal report},
url =		 {http://www-verimag.imag.fr/VHS/CS5/ilogeval.ps.gz}
}



@InProceedings{KBPST99:ifac,
author =	 {Kowalewski, S. and Bauer, N. and Preu{\ss}ig, J. and
Stursberg, O. and Treseler, H.},
title =	 {An Open Tool Architecture for the Formal
Verification of Logic Controllers in Processing
Systems},
booktitle =	 {14th IFAC World Congress},
year =	 1999,
month =	 {jul},
note =	 {Preprints},
url =
{http://www-verimag.imag.fr/VHS/resources/KBPST99.ps.gz},
abstract =	 {A tool environment for the formal verification of
logic controllers for switched continuous systems is
presented. It supports a model-based verification
approach which builds on different models of the
controller and the plant. The architecture consists
of a hierarchical plant modeling editor, a
translator for the input of controllers given in IL
code, and an interface to integrate available
model-checkers, e.g., for Timed Automata. In the
paper, each architecture component is described and
the modeling interface is illustrated by an
example.}
}



@Article{KDEH00pse,
author =	 {K.-U. Klatt and G. D{\"u}nnebier and S. Engell and
F. Hanisch},
title =	 {Model-Based Optimization and Control of
Chromatographic Processes},
journal =	 {To appear in Computers Chem. Engng},
year =	 2000,
note =	 {Supplement to PSE2000},
url =		 {http://www-verimag.imag.fr/VHS/CS3/pse_final.pdf}
}



@Article{KEPS99:automatica,
author =	 {Kowalewski, S. and Engell, S. and Preu{\ss}ig, J. and
Stursberg, O.},
title =	 {Verification of Logic controllers for Continuous
Plants Using Timed Condition/Event-System Models},
journal =	 {Automatica},
year =	 1999,
volume =	 35,
number =	 3,
pages =	 {505--518},
month =	 {mar},
note =	 {Special Issue on Hybrid Systems},
url =		 {http://www-verimag.imag.fr/VHS/resources/KEPS99.pdf},
abstract =	 {An approach to the formal verification of logic
controllers for processes with switched continuous
dynamics is presented. The method builds on modular,
timed discrete event models of the plant and the
controller. Subsystems with continuous dynamics are
approximated algorithmically. The formal
verification consists of determining the reachable
discrete states of the resulting model and comparing
it to a set of undesired states. For this purpose,
the tool HyTech is applied. The approach is
illustrated by the treatment of a process
engineering example.}
}



@Article{KHD00control,
author =	 {K.-U. Klatt, F. Hanisch, G. D{\"u}nnebier},
title =	 {Model-Based Control of a Simulated Moving Bed
Chromatographic Process for the Separation of
Fructose and Glucose},
journal =	 {Submitted to Journal of Process Control},
year =	 2000,
url =
{http://www-verimag.imag.fr/VHS/CS3/jpc_submitted.pdf}
}



@InProceedings{KLLU98:wodes,
author =	 {Kowalewski,S. and Lakhnech, Y. and Lukoschus, B. and
Urbina, L.},
title =	 {On the composition of condition/event systems},
booktitle =	 {Proceedings 4th Workshop on Dsicrete Event Systems
(WODES 98)},
pages =	 {349--354},
year =	 1998,
month =	 {aug},
organization = {IEE},
url =
{http://www.informatik.uni-kiel.de/~kondisk/wodes98.ps.gz},
abstract =	 {In this paper, several aspects of the composition of
discrete state condition/event systems according to
Sreenivas and Krogh are discussed. We introduce a
new composition operator called parallel
interconnection. It is shown to be a generalization
of the originally defined cascade and feedback
operators. Based on this composition operator, a
modular refinement rule is presented which can be
used to prove that a parallel interconnection of
condition/event systems refines a given other one.}
}



@unpublished{KLPW99:cs1,
author =	 {K. Kristoffersen and K. Larsen and P. Pettersson and
C. Weise},
title =	 {{VHS Case Study 1 - Experimental Batch Plant using
UPPAAL}},
note =	 {BRICS, University of Aalborg, Denmark},
month =	 {May},
year =	 {1999},
url =
{http://www.cs.auc.dk/research/FS/VHS/cs1uppaal.ps.gz}
}



@InProceedings{KS99:wodes,
author =	 {Stefan Kowalewski and Olaf Stursberg},
title =	 {The batch evaporator: A benchmark example for safety
analysis of processing systems under logic control},
booktitle =	 {Proceedings 4th Workshop on Discrete Event Systems
(WODES)},
pages =	 {302--307},
year =	 1998,
url =		 {http://www-verimag.imag.fr/VHS/year1/cs11d.ps},
organization = {IEE, London}
}



@unpublished{Kowa98:cs1descr,
author =	 {S. Kowalewski},
title =	 {Description of {VHS} Case Study 1 "{Experimental
Batch Plant}"},
note =	 {Draft. University of Dortmund, Germany},
month =	 {July},
url =
{http://astwww.chemietechnik.uni-dortmund.de/~vhs/cs1descr.zip},
year =	 {1998}
}



@Inproceedings{Kowa99:wfmm,
author =	 {Stefan Kowalewski},
title =	 {Formal methods and the processing industries: status
and prospects from an academic perspective},
booktitle =	 {Workshop on Formal Methods and Manufacturing},
year =	 1999,
pages =	 {75--91},
url =
{http://www-verimag.imag.fr/VHS/resources/wfmm_zaragoza_99.pdf},
publisher =	 {University of Zaragoza}
}



@inproceedings{Kronos98,
author =	 {M.~Bozga and C.~Daws and O.~Maler and A.~Olivero and
S.~Tripakis and S.~Yovine},
title =	 {Kronos: A model-checking tool for real-time systems},
booktitle =	 {Proc. 1998 Computer-Aided Verification, CAV'98},
month =	 {June},
year =	 1998,
series =	 {Lecture Notes in Computer Science},
volume =	 {1427},
publisher =	 {Springer-Verlag},
abstract =	 {},
URL =
{http://www-verimag.imag.fr/~yovine/articles/rts_embedded98.ps.gz}
}



@techreport{LSVW99,
author =	 {N.A. Lynch and R. Segala and F.W. Vaandrager and
H.B. Weinberg},
title =	 {Hybrid {I/O} Automata},
year =	 1999,
month =	 may,
type =	 {Report},
institution =	 {Computing Science Institute, University of Nijmegen},
number =	 {CSI-R9907},
url =		 {http://www.cs.kun.nl/~fvaan/PAPERS/LSVWfull.ps.Z},
abstract =	 { We propose a new {\em hybrid automaton\/} model
that is capable of describing both continuous and
discrete behavior. The model, which extends the
timed automaton model of [LV96,SGSL98] and the phase
transition system models of [MMP92,AlurEtAl95],
allows communication among components using both
shared variables and shared actions. The main
contributions of this paper are: (1) a definition of
hybrid automata and of an implementation relation
based on {\em hybrid traces\/}, (2) a definition of
a {\em simulation\/} between hybrid automata and a
proof that existence of a simulation implies the
implementation relation, (3) a definition of {\em
composition\/} and {\em hiding\/} operations on
hybrid automata and a proof that these operations
respect the implementation relation, (4) a
definition of {\em hybrid I/O automata\/}, which
specialize hybrid automata by an additional
distinction between input and output, and a proof
that the results on simulation relations,
composition and hiding carry over to this new
setting, and (5) a definition of {\em
receptiveness\/} for hybrid I/O automata and a proof
that, assuming certain compatibility conditions,
receptiveness is preserved by composition. }
}



@article{LWWP99,
author =	 "Larsen, Kim G. and Weise, Carsten and Yi, Wang and
Pearson, Justin",
title =	 "Clock Difference Diagrams",
journal =	 "Nordic Journal of Computing",
year =	 1999,
volume =	 6,
number =	 3,
pages =	 "271--298",
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/LWWP99.ps.gz}
}



@inproceedings{La00,
author =	 "Larsen, Kim G.",
title =	 "Verification of Timed and Hybrid Systems",
booktitle =	 "International Conference on Application and Theory
of Petri Nets",
year =	 2000,
pages =	 "39--42",
month =	 "",
note =	 "Invited talk",
series =	 {LNCS},
volume =	 1825,
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/La00.ps.gz}
}



@INCOLLECTION{LafferrierePappasYovine99a,
AUTHOR =	 {G. Lafferriere and G. J. Pappas and S. Yovine},
TITLE =	 {A new class of decidable hybrid systems},
BOOKTITLE =	 {Hybrid Systems : Computation and Control},
SERIES =	 {Lecture Notes in Computer Science},
PUBLISHER =	 {Springer Verlag},
VOLUME =	 {1569},
PAGES =	 {137-151},
YEAR =	 1999,
ABSTRACT =	 {One of the most important analysis problems of
hybrid systems is the reachability problem. State of
the art computational tools perform reachability
computation for timed automata, multirate automata,
and rectangular automata. In this paper, we extend
the decidability frontier for classes of linear
hybrid systems, which are introduced as hybrid
systems with linear vector fields in each discrete
location. This extension is important given the
applicability of linear vector fields in control
systems. This result is achieved by showing that any
such hybrid system admits a finite bisimulation, and
by providing an algorithm that computes it using
decision methods from mathematical logic.},
URL =
{http://www-verimag.imag.fr/~yovine/articles/hs_hs99.ps.gz}
}



@INPROCEEDINGS{LafferrierePappasYovine99b,
AUTHOR =	 {G. Lafferriere and G. J. Pappas and S. Yovine},
TITLE =	 {Reachability Computation for Linear Hybrid Systems},
BOOKTITLE =	 {Proceedings of the 14th IFAC World Congress},
VOLUME =	 {E},
PAGES =	 {7-12},
MONTH =	 jul,
YEAR =	 1999,
ABSTRACT =	 {Linear hybrid systems are finite state machines with
linear vector fields of the form x'=Ax in each
discrete location. Very recently, the reachability
problem for classes of linear hybrid systems was
shown to be decidable. In this paper, the
decidability result is extended to capture classes
of linear hybrid systems where in each location the
dynamics are of the form x'=Ax+Bu, for various types
of inputs.},
URL =
{http://www-verimag.imag.fr/~yovine/articles/hs_ifac99.ps.gz}
}



@InProceedings{LiWa00,
author =	 {Huimin Lin and Wang Yi},
title =	 {A Proof System for Timed Automata},
booktitle =	 {In the proc of FOSSACS'00},
year =	 2000,
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/LiWa00.ps.gz}
}



@TechReport{Lukoschus99a,
author =	 {Ben Lukoschus},
title =	 {Composition and Verification of Condition/Event
Systems},
institution =	 {Christian-Albrechts-Universit{\"a}t zu Kiel},
year =	 1999,
number =	 {(number to be assigned)},
url =		 {http://www-verimag.imag.fr/VHS/year1/cs11k.ps},
abstract =	 {We consider different ways of combining discrete and
timed condition/event systems (CESs) in a modular,
compositional way. In addition to the
interconnection operators for CESs found in the
literature, we introduce a new, powerful operator,
called parallel interconnection operator, which
allows arbitrary connections among a set of CESs. An
extensive example shows various possibilities how to
verify properties of a system consisting of some
interconnected CESs. We conclude this work by
showing how a set of interconnected discrete CESs
can be transformed into the input language of the
model checking tool SMV. This offers another
possibility to apply formal verification to
condition/event systems.}
}



@TechReport{Lukoschus99b,
author =	 {Ben Lukoschus},
title =	 {An Abstract Model of {VHS} Case Study 1
(Experimental Batch Plant)},
institution =	 {Christian-Albrechts-Universit{\"a}t zu Kiel},
year =	 1999,
number =	 {(number to be assigned)},
url =		 {http://www-verimag.imag.fr/VHS/year1/cs11g.ps},
abstract =	 {In this work we describe the verification of safety
properties for the experimental batch plant of case
study 1 using the model checker SMV. Discrete
condition/event systems are used to describe the
physical parts of the plant and the control
programs. This model is transformed into SMV code,
and the properties are checked.}
}



@inproceedings{MaWu99:timedautomataforplcs,
author =	 {Angelika Mader and Hanno Wupper},
title =	 {Timed Automaton Models for Simple Programmable Logic
Controllers},
booktitle =	 {Proceedings of Euromicro Conference on Real-Time
Systems 1999},
month =	 {june, 9-11},
year =	 1999,
note =	 {to appear},
abstract =	 { We give timed automaton models for a class of
Programmable Logic Controller (PLC) applications,
that are programmed in the Boolean fragment of the
language Instruction Lists as defined in the
standard IEC 1131-3. Two different approaches for
modelling timers are suggested, that lead to two
different timed automaton models. The purpose of
this work is to provide a basis for verification and
testing of real-time properties of PLC
applications. Our work can be seen in broader
context: it is a contribution to methodical
development of provably correct programs. Even if
the present PLC hardware will be substituted by
e.g. Personal Computers, with a similar operation
mode, the development and verification method will
remain useful.}
}



title =	 {A Classification of {PLC} Models and Applications},
booktitle =	 {Proceedings 5th Workshop on Discrete Event Systems
(WODES2000), {\rm August 21-23, 2000, Gent,
Belgium}},
year =	 2000,
abstract =	 {In the past years there is an increasing interest in
analysing PLC applications with formal methods. The
first step to this end is to get formal models of
PLC applications. Meanwhile, various models for PLCs
have already been introduced in the literature. In
our paper we discuss several classification criteria
that characterise different ways of modelling. The
criteria include the PLC execution mechanism, the
treatment of time and language fragments used. We
try to motivate by examples which models are useful
for which class of applications. Finally, we briefly
reflect on a number of models from the literature
according to the criteria discussed. }
}



author =	 {Angelika Mader and Ed Brinksma},
title =	 {Verification and Optimization of a {PLC} Control
Schedule},
note =	 {Submitted to {\em SPIN2000}},
year =	 2000,
abstract =	 {We report on the use of the SPIN model checker for
both the verification of a process control program
and the derivation of optimal control
schedules. This work was carried out as part of a
case study for the EC VHS project (Verification of
Hybrid Systems), in which the program for a
Programmable Logic Controller (PLC) of an
experimental chemical plant had to be designed and
verified. The intention of our approach was to see
how much could be achieved here using the standard
model checking environment of SPIN/Promela. As the
symbolic calculations of real-time model checkers
can be quite expensive it is interesting to try and
exploit the efficiency of established non-real-time
model checkers like SPIN in those cases where
promising work-arounds seem to exist. In our case we
handled the relevant real-time properties of the PLC
controller using a time-abstraction technique; for
the scheduling we implemented in Promela a so-called
{\em variable time advance procedure\/}. For this
case study these techniques proved sufficient to
verify the design of the controller and derive
(time-)optimal schedules with reasonable time and
space requirements.}
}



author =	 {Angelika Mader and Ed Brinksma and Hanno Wupper and
Nanette Bauer},
title =	 {Design of a {PLC} Control Program for a Batch Plant,
{VHS} Case Study 1},
note =	 {Submitted for journal publication},
year =	 2000,
validation of a PLC control program for the batch
plant that has been selected as a case study for the
EC project on Verification of Hybrid Systems
(VHS). We show how a correct design of the control
program can be obtained in a stepwise manner using
the technique of \textit{systematic specification
weakening\/}. In this technique the system
specification is structured as a logical implication
whose conclusion represents the desired behaviour of
the plant. The premise of the implication
characterises the assumptions under which this
behaviour is realised. Our design procedure
strengthens the premise in a step by step fashion,
reflecting the accumulated design decisions, until
the premise yields a sufficiently detailed
description of the required program and the
implication holds true. In our elaborations we show
that using this procedure the code for a PLC
controller can be obtained in a straightforward and
natural way. Whilst the design steps require the
combination of simple logical reasoning principles
and insight in the application context (obvious
facts about the plant), the final proof of
correctness was obtained using the Spin
model-checker. The required Promela model was
obtained as a straightforward translation of the
ultimate version of the premise and the PLC code
derived from it. We conclude that the judicious use
of standard formal methods and tools suffices for
the systematic development of correct control
programmes for this kind of application.}
}



author =	 {Angelika Mader and Hanno Wupper},
title =	 {What is the formal method for {PLC} applications?},
booktitle =	 {Proceedings ADPM 2000: 4th International Conference
on Automation of Mixed Processes: Hybrid Dynamic
Systems, {\rm September 18-19, 2000, Dortmund,
Germany}},
year =	 2000,
abstract =	 {The question we try to investigate is how to get PLC
applications with confidence in their proper
functioning. Especially, we are interested in the
contribution that formal methods can provide for
their development. Our maxim is that the place of a
particular formal method in the total picture of
system development should be made very
clear. Developers and customers ought to understand
very well what they can be sure of and what not, and
we see our task in trying to make this
explicit. Therefore, for us the answer to the
question above refines to the following questions:
Which parts of the system can be treated formally?
What formal methods and tools can be applied? What
does their successful application tell (or does not
tell) about the proper functioning of the whole
system?}
}



@TechReport{Mahfoudh00,
author =	 {Moez Mahfoudh},
title =	 {R{\'e}solution des Probl{\'e}mes d'Ordonnancement {\a} l'aide
de Poly{\'e}dres Temporis{\'e}s},
institution =	 {VERIMAG},
year =	 2000,
url =
{http://www-verimag.imag.fr/VHS/resources/mahfoudh00.ps.gz}
}



@InProceedings{Maler98:unified,
author =	 {O.~Maler},
title =	 {A Unified Approach for Studying Discrete and
Continuous Dynamical Systems},
booktitle =	 {CDC'98},
year =	 1998,
publisher =	 {IEEE},
month =	 {December},
url =
{http://www-verimag.imag.fr/~maler/Papers/unified.ps.gz},
abstract =	 {A Unified Approach for Studying Discrete and
Continuous Dynamical Systems. The goal of this paper
is to present discrete transition systems and
continuous dynamical systems in a uniform manner,
stressing the fundamental differences as well as the
commonalities between these two fundamental
models. Such a framework seems to be a pre-requisite
to any theory and methodology for hybrid
systems. For both types of systems we introduce
three models (a closed system, a system with one
type of input and a system with two types of input)
such that the problems associated with them
correspond respectively to the tasks of simulation,
verification and control synthesis. We will discuss
some of the computational problems associated with
}



@Unpublished{Maler99:ip,
author =	 {Oded Maler},
title =	 {On the programming of industrial computers},
note =	 {VHS deliverable in Workpackage IP.1},
month =	 {May},
url =		 {http://www-verimag.imag.fr/VHS/IP/iec1131.ps},
year =	 1999
}



@Unpublished{Maler99b:scheduling,
author =	 {Oded Maler},
title =	 {On the problem of task scheduling},
note =	 {VHS draft},
month =	 {february},
url =
{http://www-verimag.imag.fr/VHS/resources/malersched.ps.gz},
year =	 1999
}



@InProceedings{NTY00:med,
author =	 {Peter Niebert and Stavros Tripakis and Sergio
Yovine},
title =	 {Minimum-Time Reachability for Timed Automata},
booktitle =	 {IEEE Mediteranean Control Conference},
year =	 2000,
url =
{http://www-verimag.imag.fr/~niebert/pubs/med00.ps.gz},
note =	 {accepted for publication}
}



@InProceedings{NiYo00b,
author =	 {Peter Niebert and Sergio Yovine},
title =	 {Synthesis and Dispatching of Production Schemes of
Chemical Batch Plants},
booktitle =	 {to appear in proceedings of ADPM'00},
year =	 2000,
abstract =	 {We propose a computer-aided methodology to
automatically generate production schemes for
chemical batch plants operating in multi-batch
mode. Our approach is based on the following
principles: (1) the plant is modeled at the level of
process operations whose behavior is specified by
timed automata, (2) the production schemes are
generated using algorithms for reachability analysis
of timed automata implemented in
\textsc{OpenKronos}, (3) the output of the
verification tool is post-processed to derive a
dispatcher. Our method works for non-cyclic and
cyclic production. We apply our methodology to the
batch plant at the University of Dortmund. The
automatically computed operation schemes turn out to
be more efficient than the previously used
handwritten ones.},
url =
}



@Misc{NiYo99:cs1,
author =	 {Peter Niebert and Sergio Yovine},
title =	 {Computing Optimal Operation Schemes for Multi Batch
Operation of Chemical Plants},
howpublished = {VHS deliverable},
month =	 {May},
year =	 1999,
note =	 {draft},
abstract =	 { We describe a methodology for optimal controller
construction for chemical batch plants. The emphasis
lies on the problem of running multiple batches. We
consider a layered design and solution to the above
problem, in particular with a lower level layer
realised in PLCs and a higher level layer realised
on arbitrary computer systems (usually PCs), such
that the lower layer offers to the higher layer a
collection of atomic process operations. Then the
safe operation is a concern primarily addressing the
lower layer and optimisation/scheduling a concern of
the higher layer mostly. We formalise these concepts
and apply them to the case study of a student's
batch plant at the university of Dortmund. Using
several algorithmic approaches from real time
verification, we were able to compute optimal
schedules for this plant, which improve over the
url =		 {http://www-verimag.imag.fr/VHS/year1/cs11e.ps}
}



@TechReport{Nie99hydro,
author =	 {Peter Niebert},
title =	 {Compositional Modelling of Hydrodynamic Plants in
institution =	 {VERIMAG},
year =	 1999,
url =
{http://www-verimag.imag.fr/~niebert/pubs/Nie99hydro.ps.gz},
abstract =	 { In this work, we report on efforts for building a
modelling} of hydrodynamic networks. The work is
inspired by a cooperation with the EDF, where the
desire for compositional modelling in a causal
framework was exposed. The nature of the dynamics of
hydrodynamic systems itself is compositional, and it
is desirable to profit from this compositionality
for modelling. This can be of great importance for
quick production of prototype simulation models for
understanding system dynamics. We explain the
modelling technique used and how it relates to other
approaches, give examples to indicate the
construction of the prototypic simulink library and
comment on experiences gained with this model. }
}



@inproceedings{NiebertYovine00a,
author =	 {P. Niebert and S. Yovine},
title =	 {Computing Optimal Operation Schemes for Chemical
Plants in Multi-batch Mode},
booktitle =	 {Proc. Hybrid Systems, Computation and Control,
HSCC'00},
month =	 {March},
year =	 2000,
series =	 {LNCS},
volume =	 {},
publisher =	 {Springer-Verlag},
abstract =	 {We propose a computer-aided methodology to
automatically generate time- and resource-optimal
production schemes for chemical batch plants
operating in multi-batch mode. Our approach is based
on the following principles: (1) the plant is
modeled at the level of process operations whose
behavior is specified by timed automata, (2) the
optimal production schemes are generated using the
algorithms for reachability analysis of timed
automata implemented in \textsc{OpenKronos}, (3) the
output of the verification tool is post-processed to
derive high-level control code. We apply our
methodology to the batch plant at the University of
Dortmund. The automatically computed operation
schemes turned out to be more efficient than the
ones obtained following the standard approach.},
URL =
{http://www-verimag.imag.fr/~niebert/pubs/hscc00.ps.gz}
}



@InProceedings{PKHW98:ftrtft,
author =	 {Preu{\ss}ig, J. and Kowalewski, S. and Henzinger,
T. A. and Wong-Toi, H.},
title =	 {An algorithm for the approximate analysis of simple
rectangular automata},
booktitle =	 {5th Int. School and Symposium on Formal Techniques
in Fault Tolerant and Real Time Systems},
pages =	 {228--240},
year =	 1998,
number =	 1486,
series =	 {Lecture Notes in Computer Science},
publisher =	 {Springer},
url =
{http://www-verimag.imag.fr/VHS/resources/PKHW98.ps.gz},
abstract =	 {Rectangular automata are well suited for approximate
modeling of continuous--discrete systems. The exact
analysis of these automata is feasible for small
examples but can encounter severe numerical problems
for even medium-sized systems. This paper presents
an analysis algorithm that uses conservative
overapproximation to avoid these numerical
problems. The algorithm is demonstrated on a simple
benchmark system consisting of two connected tanks.}
}



@InProceedings{PSK99:hscc,
author =	 {Preu{\ss}ig, J. and Stursberg, O. and Kowalewski, S.},
title =	 {Reachability Analysis of a Class of Switched
Continuous Systems by Integrating Rectangular
Approximation and Rectangular Analysis},
booktitle =	 {2nd Int. Workshop on Hybrid Systems: Computation and
Control},
year =	 1999,
number =	 1569,
series =	 {Lecture Notes in Computer Science},
month =	 {mar},
publisher =	 {Springer},
url =
{http://www-verimag.imag.fr/VHS/resources/PSK99.ps.gz},
abstract =	 {The paper presents a concept for the reachability
analysis of switched continuous systems in which
switching only occurs when the continuous state
trajectory crosses thresholds defined by a
rectangular partitioning of the state space. It
combines an existing approach for approximating such
systems by rectangular automata with an existing
reachability algorithm for this class of hybrid
automata. Instead of creating a complete abstraction
of the original system by a rectangular automaton
first and then analyzing it, in the presented
procedure the flow conditions of the visited
locations are determinded on-the-fly during the
course of the analysis. The algorithm is illustrated
with the help of a simple physical example.}
}



@article{PeLa00,
author =	 "Paul Pettersson and Kim G. Larsen.",
title =	 "{Uppaal}2k",
journal =	 "Bulletin of the European Association for Theoretical
Computer Science",
year =	 2000,
volume =	 70,
pages =	 "40--44",
month =	 feb,
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/lp-eatcs2000.ps.gz}
}



@InProceedings{RaRi99,
author =	 "Ravn, Anders P. and Rischel, Hans",
title =	 "Real-Time Constraints Through the {ProCoS} Layers",
booktitle =	 {Correct System Design Recent Insights and Advances},
series =	 {LNCS},
year =	 1999,
volume =	 1710,
pages =	 "61--78",
key =		 "embedded system, hybrid system, real-time,
requirements, design, formal specification.",
abstract =	 "The Provably Correct Systems project developed links
between layers of formal specifications for
real-time systems. These layers cover requirements
capture, design, programming and code generation. In
this paper we trace real-time constraints through
the layers in order to inspect their changing
forms. They originate in constraints on continuous
dynamical models of physical phenomena. However, in
a digital system it is desirable to abstract the
complexities of these models to simple clocks, and
further to events in a reactive system. This
paradigm is the main topic of this paper. We
illustrate the different forms of timing constraints
in duration calculus, a real-time interval logic.",
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/RaRi99.ps.gz}
}



@InProceedings{RoRa99,
author =	 "R{\"o}nkk{\"o}, Mauno and Ravn, Anders P.",
title =	 "Action Systems with Continuous Behaviour",
booktitle =	 "Hybrid Systems V",
year =	 1999,
pages =	 "304--323",
series =	 "LNCS",
volume =	 1567,
abstract =	 "An action system framework is a predicate
transformer based method for modelling and analysing
distributed and reactive systems. The actions are
statements in Dijkstra's guarded command language,
and their semantics is given by predicate
transformers. We extend conventional action systems
with a differential action consisting of a
differential equation and an evolution guard. The
semantics is given by a weakest liberal precondition
transformer, because it is not always desirable that
differential actions terminate. It is shown that the
proposed differential action has a semantics which
corresponds to a discrete approximation when the
discrete step size goes to zero. The extension gives
action systems the power to model real-time clocks
and continuous evolutions within hybrid systems. In
this paper we give a standard form for such a hybrid
action system. We also extend parallel composition
to hybrid action systems. This does not change the
original meaning of the parallel composition, and
therefore ordinary action systems compose in
parallel with hybrid action systems.",
comment =	 "Also
http://www.tucs.abo.fi/publications/techreports/TR151.html",
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/RoRa99.ps.gz}
}



@InProceedings{SEK99:ifac,
author =	 {Stursberg, O. and Engell, S. and Kowalewski, S.},
title =	 {Timed Approximating of Hybrid Processes for
Controller Verification},
booktitle =	 {Preprints 14th IFAC World Congress},
year =	 1999,
month =	 jul,
url =
{http://www-verimag.imag.fr/VHS/resources/SEK99.ps.gz},
abstract =	 {An approach to the formal verification of logic
controllers for processes with switched continuous
dynamics is presented. The method builds on modular,
timed discrete event models of the plant and the
controller. Subsystems with continuous dynamics are
approximated algorithmically. The formal
verification consists of determining the reachable
discrete states of the resulting model and comparing
it to a set of undesired states. For this purpose,
the tool HyTech is applied. The approach is
illustrated by the treatment of a process
engineering example.}
}



@InProceedings{SK99:ecc,
author =	 {Stursberg, O. and Kowalewski, S.},
title =	 {Approximating Switched Continous Systems by
Rectangular Automata},
booktitle =	 {Proceedings ECC'99},
year =	 1999,
url =		 {http://www-verimag.imag.fr/VHS/resources/SK99.ps.gz},
month =	 {sep}
}



@article{SLAHBKLL00,
author =	 "Staunstrup, J{\o}rgen and Larsen, Kim G. and Andersen,
Henrik Reif and Hulgaard, Henrik and Behrmann, Gerd
and Kristoffersen, K{\aa}re J. and Lind-Nielsen, J{\o}rn
and Leerberg, Henrik",
title =	 "Practical Verification of Embedded Software",
journal =	 "IEEE Computer",
year =	 2000,
month =	 may,
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/SLAHBKLL00.ps.gz}
}



@inproceedings{SV99a,
author =	 {M.I.A. Stoelinga and F.W. Vaandrager},
title =	 {Root Contention in {IEEE} 1394},
booktitle =	 {Proceedings of the 5th {AMAST} Workshop on Real-Time
and Probabilistic Systems, {\rm Bamberg, Germany}},
editor =	 {J.-P. Katoen},
publisher =	 {Springer},
series =	 {LNCS},
volume =	 1601,
year =	 1999,
url =		 {http://www.cs.kun.nl/~fvaan/PAPERS/arts.ps.Z},
abstract =	 { The model of probabilistic I/O automata of Segala
and Lynch is used for the formal specification and
analysis of the root contention protocol from the
physical layer of the IEEE 1394 (FireWire'')
standard. In our model of the protocol both
randomization and real-time play an essential
role. In order to make our verification easier to
understand we introduce several intermediate
automata in between the implementation and the
specification automaton. This allows us to use very
simple notions of refinement rather than the more
general but also very complex simulation relations
which have been proposed by Segala and Lynch. }
}



@InCollection{St1:00,
author =	 {G. Stremersch},
title =	 {Linear and integer programmes in supervisory control
of {Petri} nets},
booktitle =	 {Discrete Event Systems Modelling and Analysis},
pages =	 {325-332},
year =	 {2000},
url =
{http://www-verimag.imag.fr/VHS/resources/St100.ps.gz},
abstract =	 {Constructing supervisors for Petri nets of which the
uncontrollable part is acyclic can be done by
solving linear integer programme. In this paper, we
construct a closed-form solution of the
corresponding linear programme and provide in this
way a lower bound of the supremal controllable
subset of the legal set. Further, we show that in a
lot of cases this technique can be used to construct
a closed-form solution of the original linear
integer programme. We recover existing results in
supervisory control and show how to treat a class of
acyclic nets containing both choice places and a
synchronising transition.}
}



@InProceedings{St2:00,
author =	 {G. Stremersch},
title =	 {Linear algebraic design of supervisors for partially
observed {Petri} nets},
booktitle =	 {Proceedings of the IFAC Control Systems Design
Conference, Bratislava, Slovakia},
organization = {IFAC},
year =	 {2000},
url =
{http://www-verimag.imag.fr/VHS/resources/St200.ps.gz},
abstract =	 { The design of supervisors for Petri nets containing
both uncontrollable and unobservable transitions is
studied. The control goal is that the marking always
satisfies a linear inequality, defining a so-called
legal set. Supervisors are designed by using linear
programming techniques. One only has to find the
minimal ---w.r.t.\ the componentwise partial
order--- vertices of a polyhedron. Moreover, the
presented method allows to make an approximation of
the worst-case uncontrollable behaviour of the
original Petri net without doing any reachability
analysis.}
}



@Article{StBo1:00,
author =	 {G. Stremersch and R.K. Boel},
title =	 {Reduction of the supervisory control problem of
{Petri} nets},
journal =	 {IEEE Transactions on Automatic Control},
year =	 {2000},
url =
{http://www-verimag.imag.fr/VHS/resources/StBo100.ps.gz},
abstrtact =	 { We prove a reduction theorem for the supervisory
control problem for general Petri nets with general
legal sets. To design control laws guaranteeing that
the marking stays within the legal set, it suffices
to consider a sub-Petri net of the full model. This
extends existing design algorithms, allows us to
prove an important property of maximally permissive
control laws and limits the number of events which
must be observed.}
}



@Article{StBo2:00,
author =	 {G. Stremersch and R.K. Boel},
title =	 {Structuring acyclic {Petri} nets for reachability
analysis and control},
journal =	 { Journal of Discrete Event Dynamic Systems: Theory
and Applications},
year =	 { 2000},
url =
{http://www-verimag.imag.fr/VHS/resources/StBo200.ps.gz},
abstract =	 { The incidence matrices ---from places to
transitions and vice versa--- of an acyclic Petri
net can obtain a block-triangular structure by
reordering their rows and columns. This allows the
efficient solution of some reachability problems for
acyclic Petri nets. This result is further used in
supervisory control of Petri nets; supervisors for
Petri nets with uncontrollable transitions are
constructed by extending the method of Yamalidou
{\em et al.}\ to Petri nets where transitions can be
executed simultaneously. A large class of Petri nets
with uncontrollable transitions is given for which
the maximally permissive supervisor can be realised
by a Petri net. The original specification is
algorithmically transformed ---by using the results
for acyclic Petri nets--- into a new specification
to take the presence of uncontrollable transitions
into account. Furthermore, a class of Petri nets is
given for which the supervisor can be realised by
extending the enabling rule with OR-logic.}
}

@InProceedings {StBo2:99,
author =	 {G. Stremersch and R.K. Boel},
title =	 {Enforcing k-safeness in controlled state machines},
booktitle =	 {Proceedings of the 38th IEEE Conference on Decision
and Control},
organization = {IEEE},
pages =	 {1737-1742},
year =	 {1999},
url =
{http://www-verimag.imag.fr/VHS/resources/StBo299.ps.gz},
abstract =	 {We design a supervisor which enforces k-safeness in
state machines, i.e.\ the marking of every place is
not allowed to be greater than a natural number k,
and which is itself a Petri net. This is done by
extending the control design method based on
invariants to Petri nets which contain
uncontrollable transitions. We show that this
supervisor is maximally permissive ---disables as
few transitions as possible--- and is minimal
---contains as few control places as
possible. Finally, we show that the design of the
supervisor can be done using min-plus algebra.}
}



@InProceedings{StBo:98,
author =	 {G. Stremersch and R.K. Boel},
title =	 {On the influencing net and forbidden state control
of timed {Petri} nets with forced transitions},
booktitle =	 {Proceedings of the 37th IEEE Conference on Decision
and Control},
pages =	 {3287--3292},
organization = {IEEE},
year =	 {1998},
url =		 {http://www-verimag.imag.fr/VHS/resources/SB98.ps.gz},
abstract =	 {In this paper we discuss forbidden state feedback
control design for real-time discrete event systems
modeled by timed Petri nets. The firing time of a
state-enabled transition lies in an interval which
can be modified for controllable transitions. Once
the upper bound is reached, the transition,
controllable or uncontrollable, is forced to
fire. We construct necessary and sufficient
conditions for the control to satisfy forbidden
state control objectives for the case of a timed
marked graph. From these equations we derive what
the influencing net looks like.}
}

@InProceedings {StBo:99,
author =	 {G. Stremersch and R.K. Boel},
title =	 {Controlled {Petri} nets and general legal sets},
booktitle =	 {Proceedings of the 38th IEEE Conference on Decision
and Control},
organization = {IEEE},
pages =	 {1731-1736},
year =	 {1999},
url =
{http://www-verimag.imag.fr/VHS/resources/StBo99.ps.gz},
abstract =	 {This paper proves a reduction theorem for the
supervisory control of general controlled Petri
nets, with general legal sets. The reduction theorem
shows that in order to design a maximally permissive
control law guaranteeing that the marking alway
remains in the legal set, it is sufficient to
consider a sub-Petri net of the full model. This
extends the design algorithms which were previously
known for special classes of Petri nets, and for
special classes of legal sets. The reduction theorem
allows us to prove a useful property of maximally
permissive control laws, and to limit the number of
events which must be observed.}
}



@Unpublished{Stobbe:00,
author =	 {M. Stobbe},
title =	 {Results on Scheduling the Sidmar Steel Plant Using
Constraint Programming},
note =	 {Internal report},
year =	 2000,
url =		 {http://www-verimag.imag.fr/VHS/CS5/stobbe.ps.gz}
}



@Unpublished{TCF00:cs6desc,
author =	 {Luc Thevenon, Jacques Camand, Jean-Marie Flaus},
title =	 {{VHS} Case Study 6 -- Yarn Production Process},
note =	 {Progress report},
url =		 {http://www-verimag.imag.fr/VHS/CS6/cs6descr.ps.gz},
year =	 2000
}



@Unpublished{TCF99:cs6desc,
author =	 {Luc Thevenon, Jacques Camand, Jean-Marie Flaus},
title =	 {{VHS} Case Study 6},
note =	 {preliminary draft},
month =	 {May},
url =		 {http://www-verimag.imag.fr/VHS/CS6/tcf99.ps.gz},
year =	 1999
}



@InProceedings{ThFl99:modularhybrid,
author =	 {Luc Thevenon and Jean-Marie Flaus},
title =	 {Modular and multi-view representation of complex
hybrid systems},
booktitle =	 {3rd DIMACS|IEEE International Multiconference
CSCC99},
year =	 1999,
month =	 {July},
url =
{http://www-verimag.imag.fr/VHS/resources/ThFl99.ps.gz}
}



@InProceedings{ThFl99a:modularhybrid,
author =	 {Luc Thevenon and Jean-Marie Flaus},
title =	 {Representation Modulaire et Multi-Vues De Systemes
Complexes Hybrides : Application Aux Procedes Batch},
booktitle =	 {2e conf{\'e}rence francophone de MOd{\'e}lisation et
SIMulation, MOSIM'99},
pages =	 {291--296},
year =	 1999
}



@MASTERSTHESIS{Tor99,
author =	 {F.D. Torrisi},
year =	 1999,
title =	 {Model and Algorithms for Verification of Hybrid
Systems},
school =	 {University of Florence, School of Computer
Engineering},
month =	 apr,
url =		 {ftp://aut.ethz.ch/pub/publications/AUTDi-99-35.pdf},
abstract =	 {Con il termine \emph{sistemi ibridi} si intendono
sistemi che hanno parti rappresentabili attraverso
variabili continue e altre che possono assumere solo
un numero finito di configurazioni. Sistemi di
questo tipo si incontrano in molte situazioni di
interesse pratico. I metodi tradizionali di
modellizzazione, analisi e controllo sono inadeguati
a trattare questa tipologia di sistemi e lasciano
spazio a soluzioni \emph{ad hoc}. La \emph{verifica
formale} si pone come obiettivo di fornire,
possibilmente in modo automatico, la garanzia che un
sistema ibrido soddisfi certe propriet{\a}. {\E} stato
affrontato il problema della verifica per sistemi
ibridi in forma \emph{mista logica dinamica
(MLD)}. La forma MLD permette di esprimere sistemi
che integrano una parte logica ad una parte dinamica
lineare. {\E} stato proposto un semi-algoritmo che, in
caso termini, permette di risolvere il problema di
verifica per i sistemi in forma MLD. Per la
caratterizzazione dell'insieme raggiungibile e la
rivelazione delle commutazioni logiche sono state
sfruttate tecniche di calcolo poliedrale e di
programmazione matematica. Abbiamo applicato
l'algoritmo proposto ad un caso di studio presente
in letteratura ottenendo risultati meno conservativi
di quelli offerti dalle tecniche di verifica
attualmente disponibili. I tempi di calcolo
necessari per portare a termine la verifica sono
risultati confrontabili con quelli riportati usando
altri pacchetti software disponibili. },
}



@inproceedings{Tripakis99,
author =	 {S. Tripakis},
title =	 {Timed Diagnostics for Reachability Properties},
booktitle =	 {Tools and Algorithms for the Construction and
Analysis of Systems, TACAS'99},
year =	 1999,
abstract =	 {},
URL =
{http://www-verimag.imag.fr/~tripakis/diagnostics.ps.gz}
}



@Misc{VHS-homepage,
key =		 {VHS},
note =	 {\texttt{http://www-verimag.imag.fr/VHS}}
}



@InProceedings{YCKS00,
author =	 {S.H. Yang and P.W.H. Chung and S. Kowalewski and
O. Stursberg},
title =	 {Automatic Safety Analysis of Computer Controlled
Plants using Model Checking},
booktitle =	 {Proc. 10th Symposium on Computer Aided Process
Engineering (ESCAPE 10)},
year =	 2000,
url =
{http://www-verimag.imag.fr/VHS/resources/yangchungetal_escape2000.pdf}
}



@inproceedings{Yovine98,
author =	 "S.~Yovine",
title =	 " Model-checking timed automata",
booktitle =	 {Embedded Systems},
publisher =	 {Springer-Verlag},
series =	 {Lecture Notes in Computer Science},
volume =	 {1494},
month =	 oct,
year =	 1998,
abstract =	 {The theory of \textsl{timed automata} provides a
formal framework to model and to verify the correct
functioning of \textsl{real-time} systems. Among the
different verification problems that have been
investigated within this theory, the so-called
\textsl{reachability} problem has been the most
throughly studied. This problem is stated as
follows. Given two states of the system, is there an
execution starting at one of them that reaches the
other? The first reason for studying such problem is
that \textsl{safety} properties can expressed as the
non-reachability of a set of states where the system
is consider to show an \textsl{incorrect} or
\textsl{unsafe} functioning. Second, the algorithms
developed for analyzing other classes of properties
are essentially based on the algorithms developed
for solving the reachability question. In this paper
we survey the different algorithms, data-structures
and tools that have been proposed in the literature
to solve this problem.},
URL =
{http://www-verimag.imag.fr/~yovine/articles/rts_embedded98.ps.gz}
}



@inproceedings{abbl98:testing,
author =	 {L. Aceto and P. Bouyer and A. Burgue{\~n}o and
K. Larsen},
title =	 {{ The Power of Reachability Testing for Timed
Automata}},
booktitle =	 {Appears in Arvind and Ramanujam, editors,
Foundations of Software Technology and Theoretical
Computer Science: 18th Conference, FST\&TCS '98
Proceedings, LNCS 1530},
pages =	 {245-256},
publisher =	 {Springer Verlag},
month =	 {december},
year =	 {1998},
url =
{http://www.cs.auc.dk/research/FS/VHS/brics-rs-98-48_ps.ps.gz}
}



@Unpublished{app:kronos,
author =	 {Sergion Yovine},
title =	 {A brief summary of the tool {Kronos}},
url =
{http://www-verimag.imag.fr/VHS/resources/TL-openkronos.ps.gz},
note =	 {VHS Deliverable TL.1 - Tools},
year =	 {2000}
}



@Unpublished{app:kronos-gui,
author =	 {Hou Jiamin and Sergio Yovine},
title =	 {An integrated {GUI} for {Kronos} and {Open Kronos}},
url =
{http://www-verimag.imag.fr/VHS/resources/TL-kronosgui.ps.gz},
note =	 {VHS Deliverable TL.1 - Tools},
year =	 {2000}
}



author =	 {Nanette Bauer and Stefan Kowalewski and Guido Sand},
title =	 {A case study: Multi product batch plant for the
demonstration of control and scheduling problems},
booktitle =	 {accepted to ADPM 2000},
year =	 {2000},
url =
{http://www-verimag.imag.fr/VHS/resources/bau2000.ps.gz},
abstract =	 {In this report a new laboratory plant which was
designed and built at the Process Control Laboratory
of the University of Dortmund is presented as a case
example. The purpose of the plant is to serve as a
test-bed and a demonstration medium for control and
scheduling methods for multi product batch plants. A
scheduling problem is proposed and the control
architecture which has been designed integrating
both control and scheduling aspects is described.}
}



@inproceedings{bjlw98:partialorder,
author =	 {J. Bengtsson and B. Jonsson and J. Lilius and W. Yi},
title =	 {{Partial Order Reductions for Timed Systems }},
booktitle =	 {Partial Order Reductions for Timed Systems, Nice,
France},
publisher =	 {Springer Verlag},
year =	 {1998},
url =		 {http://www.cs.auc.dk/research/FS/VHS/bjlw98.ps.gz}
}



@inproceedings{blahn99:hierarchical,
author =	 {G. Berhmann and K. G. Larsen and H. R. Andersen and
H. Hulgaard, J. L.-Nielsen},
title =	 {{ Verification of Hierarchical State/Event Systems
using Reusability and Compositionality}},
booktitle =	 {Proceedings of TACAS{\'{}}99, Amsterdam, The
Netherlands. LNCS 1579},
publisher =	 {Springer Verlag},
year =	 {1999},
url =		 {http://www.cs.auc.dk/research/FS/VHS/blahn.ps.gz}
}



@inproceedings{bllpww98:newgeneration,
author =	 {J. Bengtsson and K. G. Larsen and F. Larsson and
P. Pettersson and W. Yi and C. Weise},
title =	 {{New Generation of UPPAAL}},
booktitle =	 {Proceedings of the International Workshop on
Software Tools for Technology Transfer. Aalborg,
Denmark},
month =	 {12-13 July},
year =	 {1998},
url =		 {http://www.cs.auc.dk/research/FS/VHS/bllpww98.ps.gz}
}



@inproceedings{blpww99:cdd,
author =	 { G. Behrmann and K. Larsen and J. Pearson and
C. Weise and W. Yi},
title =	 {{Efficient Timed Reachability Analysis Using Clock
Difference Diagrams }},
booktitle =	 {Proceedings of CAV99},
pages =	 {22-24},
publisher =	 {Springer Verlag},
year =	 1999,
url =		 {http://www.cs.auc.dk/research/FS/VHS/blpww99.ps.gz}
}



@techreport{habets:vanschuppen:2000,
author =	 {L.C.G.J.M. Habets and J.H. van Schuppen},
title =	 {VHS Deliverable PA.1 - Control of piecewise-linear
hybrid systems},
type =	 {Report},
institution =	 {CWI},
year =	 {2000},
url =		 {http://www.cwi.nl/~schuppen/projects/vhs/dpa1cwi.ps},
abstract =	 {Piecewise-linear hybrid systems are useful
mathematical models for computer controlled
engineering systems. An approach to the
determination of reachability of such systems is
described. A control synthesis procedure for
piecewise-linear hybrid systems is proposed. As a
special case, control of polyhedral linear systems
is treated.}
}



@unpublished{hlp99:guided,
author =	 {Thomas Hune and Kim G. Larsen and Paul Pettersson},
title =	 {{Guided Synthesis of Control Programs using UPPAAL
for VHS Case Study 5}},
note =	 {BRICS, University of {\AA}rhus and University of
Aalborg, Denmark},
month =	 {June},
year =	 {1999},
url =		 {http://www.cs.auc.dk/research/FS/VHS/hlp99.ps.gz}
}



@inproceedings{hls99:power,
author =	 {K. Havelund and K. Larsen and A. Skou},
title =	 { Formal Verification of a Power Controller Using the
Real-Time Model Checker {UPPAAL}},
booktitle =	 {5th International AMAST Workshop on Real-Time and
Probabilistic Systems},
url =		 {http://www.cs.auc.dk/research/FS/VHS/hls99.ps.gz},
year =	 {1999}
}



@inproceedings{hune99:modelling,
author =	 {Thomas Hune},
title =	 {Modelling a real-time language},
booktitle =	 {Proceedings of FMICS},
year =	 {1999},
url =		 {http://www.cs.auc.dk/research/FS/VHS/fmics.ps.gz}
}



@InProceedings{labhkl:tacas98,
author =	 {J{\o}rn Lind-Nielsen and Henrik Reif Andersen and Gerd
Behrmann and Henrik Hulgaard and K{\aa}re
J.~Kristoffersen and Kim G.~Larsen},
title =	 {{Verification of Large State/Event Systems Using
Compositionality and Dependency Analysis}},
booktitle =	 "Proc.\ of the 4{\em th} Conference on Tools and
Algorithms for the Construction and Analysis of
Systems",
pages =	 {201--216},
year =	 {1998},
editor =	 {Bernard Steffen},
number =	 {1384},
series =	 {Lecture Notes in Computer Science},
url =		 {http://www.cs.auc.dk/~behrmann/papers/tacas98.ps.gz},
publisher =	 {Springer--Verlag}
}



@techreport{lpw99:deallocation,
title =	 {Efficient Memory De-Allocation in Real Time Model
Checking},
institution =	 {DoCS, Uppsala University},
year =	 {1999},
number =	 {99/106},
url =		 {http://www.cs.auc.dk/research/FS/VHS/lpw99.ps.gz}
}



@InProceedings{lpw:tacas00,
title =	 {{On Memory-Block Traversal Problems in Model
Checking Timed Systems}},
booktitle =	 {Proc.\ of the 6{\em th} Conference on Tools and
Algorithms for the Construction and Analysis of
Systems},
pages =	 {127--141},
year =	 2000,
editor =	 {Susanne Graf and Michael Schwartzbach},
number =	 1785,
series =	 {Lecture Notes in Computer Science},
publisher =	 {Springer--Verlag},
url =
{http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/lpw-tacas00.ps.gz}
}



@techreport{lwyp98:cdd,
author =	 {K. G. Larsen and C. Weise and W. Yi and J. Pearson},
title =	 {Clock Difference Diagrams},
institution =	 {DoCS, Uppsala University},
month =	 {august},
year =	 {1999},
number =	 {98/99, ISSN 0283-0574},
url =		 {http://www.cs.auc.dk/research/FS/VHS/lwyp.ps.gz}
}



@inproceedings{schuppen:1998:cdc98,
author =	 "J.H. van Schuppen",
title =	 "Coordination control of parallel operations in a
hybrid control system",
editor =	 "",
booktitle =	 "37th IEEE Conference on Decision and Control",
publisher =	 "IEEE Press",
year =	 "1998",
pages =	 "2095-2100",
class =	 "m93h89"
}



@inproceedings{schuppen:1998:hscc98,
author =	 "J.H. van Schuppen",
title =	 "A sufficient condition for controllability of a
class of hybrid systems",
editor =	 "T.A. Henzinger and S. Sastry",
booktitle =	 "Hybrid systems: Computation and control",
series =	 "Lecture Notes in Computer Science",
number =	 "1386",
publisher =	 "Springer",
year =	 "1998",
pages =	 "374-383",
class =	 "m93s89"
}



@incollection{schuppen:1998:openprob,
author =	 "J.H. van Schuppen",
title =	 "Equivalences of discrete-event systems and of hybrid
systems",
editor =	 "V.D. Blondel and E.D. Sontag and M. Vidyasagar and
J.C. Willems",
booktitle =	 "Open problems in mathematical systems and control
theory",
publisher =	 "Springer",
year =	 "1998",
pages =	 "251-257",
class =	 "m93h45 m93h49"
}



@inproceedings{schuppen:1998:wodes98,
author =	 "J.H. van Schuppen",
title =	 "Decentralized supervisory control with information
structures",
editor =	 "",
booktitle =	 "Proceedings International Workshop on Discrete Event
Systems (WODES98)",
publisher =	 "IEE",
year =	 "1998",
pages =	 "36-41",
class =	 "m93s86"
}



@InProceedings{tripakis:altisen:1999:fm99,
author =	 {S. Tripakis and K. Altisen},
title =	 {On-the-fly controller synthesis for discrete and
dense time systems},
booktitle =	 {Formal Methods 1999 (FM'99)},
pages =	 {233--252},
year =	 {1999},
series =	 {LNCS 1706},
volume =	 {I},
month =	 {September},
publisher =	 {Springer},
url =
{http://www-verimag.imag.fr/VHS/resources/AlTr99.ps.gz},
abstract =	 {We present novel techniques for efficient controller
synthesis for untimed and timed systems with respect
to invariance and reachability properties. In the
untimed case, we give algorithms for controller
synthesis in the context of finite graphs with {\em
controllable\/} and {\em uncontrollable\/} edges,
distinguishing between the actions of the system and
its environment, respectively. The algorithms are
{\em on-the-fly\/}, since they return a controller
as soon as one is found, which avoids the generation
of the whole state space. In the timed case, we use
the model of {\em timed automata\/} extended with
controllable and uncontrollable discrete
transitions. Our controller-synthesis method here is
only half on-the-fly, since it relies on the
a-priori generation of a finite model (graph) of the
timed automaton, as quotient of the {\em
time-abstracting bisimulation\/}. The quotient graph
is essentially an untimed graph, upon which we can
apply the untimed on-the-fly algorithms to compute a
timed controller.}
}



@book{vaandrager:schuppen:1999:hscc99,
editor =	 "F.W. Vaandrager and J.H. van Schuppen",
title =	 "{Hybrid systems - Computation and control}",
series =	 "Lecture Notes in Computer Science",
volume =	 1569,
publisher =	 "Springer",