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
                  arbitrarily designed tasks (cyclic or sporadic, with
                  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},
  address =	 {Phoenix, AZ},
  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,
  address =	 {Catania (Italy)},
  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},
  publisher =	 {Kluwer Academic Publishers},
  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 =
                  {http://www.informatik.uni-kiel.de/~softtech/vhs/ADPM2000.ps.gz},
  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},
  address =	 {ETH Zurich, Switzerland},
  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},
  address =	 {Chicago},
  publisher =	 {Springer-Verlag},
  url =
                  {http://www.cs.auc.dk/research/FS/VHS/vhs2/papers/bhv-cav2000.ps.gz}
}


@incollection{BeMo99-2,
  author =	 {A.~Bemporad and M.~Morari},
  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},
  booktitle =	 {Proceedings of ADPM2000},
  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.}
}


@InProceedings{BozgaMalerTripakis99:Stari,
  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.}
}


@Unpublished{Deparade99,
  author =	 {Deparade, A.},
  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,
  address =	 {London},
  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},
  address =	 {Vancouver, Canada},
  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},
  ADDRESS =	 {Beijing, P.R. China},
  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,
  address =	 {York, UK},
  note =	 {to appear},
  url =		 {http://www.cs.kun.nl/~mader/euromicro.ps},
  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.}
}


@InProceedings{Mader00:classification,
  author =	 {Angelika Mader},
  title =	 {A Classification of {PLC} Models and Applications},
  booktitle =	 {Proceedings 5th Workshop on Discrete Event Systems
                  (WODES2000), {\rm August 21-23, 2000, Gent,
                  Belgium}},
  publisher =	 {Kluwer Academic Publishers},
  year =	 2000,
  url =		 {http://www.cs.kun.nl/~mader/papers/wodes2000.ps.gz},
  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. }
}


@unpublished{MaderB00:cs1,
  author =	 {Angelika Mader and Ed Brinksma},
  title =	 {Verification and Optimization of a {PLC} Control
                  Schedule},
  note =	 {Submitted to {\em SPIN2000}},
  year =	 2000,
  url =		 {http://www.cs.kun.nl/~mader/papers/spin.ps.gz},
  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.}
}


@unpublished{MaderEtAl00:cs1,
  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,
  url =		 {http://www.cs.kun.nl/~mader/papers/cs1.ps.gz},
  abstract =	 {This article reports on the systematic design and
                  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.}
}


@InProceedings{MaderW00:method,
  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,
  url =		 {http://www.cs.kun.nl/~mader/papers/methods.ps.gz},
  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
                  building control CAD tools that carry these tasks.}
}


@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 =
                  {http://www-verimag.imag.fr/~niebert/pubs/adpm00.ps.gz}
}


@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
                  previously used ad hoc schedules.},
  url =		 {http://www-verimag.imag.fr/VHS/year1/cs11e.ps}
}


@TechReport{Nie99hydro,
  author =	 {Peter Niebert},
  title =	 {Compositional Modelling of Hydrodynamic Plants in
                  Simulink},
  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
                  prototype simulink library for \emph{compositional
                  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},
  address =	 {Pittsburgh, PA, USA},
  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},
  address =	 {Berlin},
  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},
  address =	 {Berlin},
  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},
  publisher =	 {Kluwer Academic Press},
  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},
  address =	 {Florence, Italy},
  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},
  address =	 {Amsterdam, Holland},
  year =	 1999,
  abstract =	 {},
  URL =
                  {http://www-verimag.imag.fr/~tripakis/diagnostics.ps.gz}
}


@Misc{VHS-homepage,
  key =		 {VHS},
  title =	 {The {VHS} project home page},
  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}
}


@InProceedings{bau2000adpm,
  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},
  address =	 {Amsterdam},
  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,
  author =	 {F. Larsson and P. Pettersson and W. Yi},
  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,
  author =	 {Fredrik Larsson and Paul Pettersson and Wang Yi},
  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",
  address =	 "New York",
  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",
  address =	 "Berlin",
  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",
  address =	 "London",
  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",
  address =	 "London",
  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},
  address =	 {Toulouse, France},
  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",
  address =	 "Berlin",
  year =	 "1999",
  class =	 "m93h49 m93s89"
}



page created at Tue Jun 1 14:54:58 MET DST 1999 by Peter Niebert
last modification: Thu Jun 29 15:31:29 CEST 2000