@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