ref_des.bib

@book{acetoReactiveSystemsModelling2007,
  title = {Reactive {{Systems}}: {{Modelling}}, {{Specification}} and {{Verification}}},
  shorttitle = {Reactive {{Systems}}},
  author = {Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna and Larsen, Kim G. and Srba, Ji{\v r}{\'i}},
  year = {9 srpna 2007},
  publisher = {Cambridge University Press},
  address = {New York},
  url = {https://rsbook.cs.aau.dk},
  abstract = {Formal methods is the term used to describe the specification and verification of software and software systems using mathematical logic. Various methodologies have been developed and incorporated into software tools. An important subclass is distributed systems. There are many books that look at particular methodologies for such systems, e.g. CSP, process algebra. This book offers a more balanced introduction for graduate students that describes the various approaches, their strengths and weaknesses, and when they are best used. Milner's CCS and its operational semantics are introduced, together with notions of behavioral equivalence based on bisimulation techniques and with variants of Hennessy-Milner modal logics. Later in the book, the presented theories are extended to take timing issues into account. The book has arisen from various courses taught in Iceland and Denmark and is designed to give students a broad introduction to the area, with exercises throughout.},
  isbn = {978-1-107-41068-8}
}

@article{alurTheoryTimedAutomata1994,
  title = {A Theory of Timed Automata},
  author = {Alur, Rajeev and Dill, David L.},
  year = {1994},
  month = apr,
  journal = {Theoretical Computer Science},
  volume = {126},
  number = {2},
  pages = {183--235},
  issn = {0304-3975},
  doi = {10.1016/0304-3975(94)90010-8},
  url = {https://www.sciencedirect.com/science/article/pii/0304397594900108},
  urldate = {2023-09-01},
  abstract = {We propose timed (finite) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words--infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both B{\"u}chi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable ({$\Pi$}11-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems.}
}

@inproceedings{alurTimedAutomata1999,
  title = {Timed {{Automata}}},
  booktitle = {Computer {{Aided Verification}}},
  author = {Alur, Rajeev},
  editor = {Halbwachs, Nicolas and Peled, Doron},
  year = {1999},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  pages = {8--22},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/3-540-48683-6_3},
  url = {https://doi.org/10.1007/3-540-48683-6_3},
  abstract = {Model checking is emerging as a practical tool for automated debugging of complex reactive systems such as embedded controllers and network protocols (see [23] for a survey). Traditional techniques for model checking do not admit an explicit modeling of time, and are thus, unsuitable for analysis of real-time systems whose correctness depends on relative magnitudes of different delays. Consequently, timed automata [7] were introduced as a formal notation to model the behavior of real-time systems. Its definition provides a simple way to annotate state-transition graphs with timing constraints using finitely many real-valued clock variables. Automated analysis of timed automata relies on the construction of a finite quotient of the infinite space of clock valuations. Over the years, the formalism has been extensively studied leading to many results establishing connections to circuits and logic, and much progress has been made in developing verification algorithms, heuristics, and tools. This paper provides a survey of the theory of timed automata, and their role in specification and verification of real-time systems.},
  isbn = {978-3-540-48683-1},
  langid = {english}
}

@book{andersonAutomataTheoryModern2006,
  title = {Automata {{Theory}} with {{Modern Applications}}},
  author = {Anderson, James A.},
  year = {2006},
  month = jul,
  publisher = {Cambridge University Press},
  address = {Cambridge},
  url = {https://doi.org/10.1017/CBO9780511607202},
  abstract = {Recent applications to biomolecular science and DNA computing have created a new audience for automata theory and formal languages. This is the only introductory book to cover such applications. It begins with a clear and readily understood exposition of the fundamentals that assumes only a background in discrete mathematics. The first five chapters give a gentle but rigorous coverage of basic ideas as well as topics not found in other texts at this level, including codes, retracts and semiretracts. Chapter 6 introduces combinatorics on words and uses it to describe a visually inspired approach to languages. The final chapter explains recently-developed language theory coming from developments in bioscience and DNA computing. With over 350 exercises (for which solutions are available), many examples and illustrations, this text will make an ideal contemporary introduction for students; others, new to the field, will welcome it for self-learning.},
  isbn = {978-0-521-84887-9},
  langid = {english}
}

@book{baccelliSynchronizationLinearityAlgebra2001,
  title = {Synchronization and Linearity: An Algebra for Discrete Event Systems},
  shorttitle = {Synchronization and Linearity},
  author = {Baccelli, Fran{\c c}ois and Cohen, Guy and Olsder, Geert Jan and Quadrat, Jean-Pierre},
  year = {2001},
  edition = {Web edition},
  publisher = {Wiley},
  address = {Chichester},
  url = {https://www.rocq.inria.fr/metalau/cohen/documents/BCOQ-book.pdf},
  isbn = {978-0-471-93609-1},
  langid = {english}
}

@incollection{behrmannTutorialUppaal2004,
  title = {A {{Tutorial}} on {{Uppaal}}},
  booktitle = {Formal {{Methods}} for the {{Design}} of {{Real-Time Systems}}},
  author = {Behrmann, Gerd and David, Alexandre and Larsen, Kim G.},
  editor = {Bernardo, Marco and Corradini, Flavio},
  year = {2004},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  number = {3185},
  pages = {200--236},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/978-3-540-30080-9_7},
  url = {https://doi.org/10.1007/978-3-540-30080-9_7},
  urldate = {2023-08-31},
  abstract = {This is a tutorial paper on the tool Uppaal. Its goal is to be a short introduction on the flavour of timed automata implemented in the tool, to present its interface, and to explain how to use the tool. The contribution of the paper is to provide reference examples and modelling patterns.},
  isbn = {978-3-540-23068-7 978-3-540-30080-9},
  langid = {english}
}

@incollection{bengtssonTimedAutomataSemantics2004,
  title = {Timed {{Automata}}: {{Semantics}}, {{Algorithms}} and {{Tools}}},
  shorttitle = {Timed {{Automata}}},
  booktitle = {Lectures on {{Concurrency}} and {{Petri Nets}}: {{Advances}} in {{Petri Nets}}},
  author = {Bengtsson, Johan and Yi, Wang},
  editor = {Desel, J{\"o}rg and Reisig, Wolfgang and Rozenberg, Grzegorz},
  year = {2004},
  series = {Lecture {{Notes}} in {{Computer Science}}},
  number = {3098},
  pages = {87--124},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  doi = {10.1007/978-3-540-27755-2_3},
  url = {https://doi.org/10.1007/978-3-540-27755-2_3},
  urldate = {2023-08-31},
  abstract = {This chapter is to provide a tutorial and pointers to results and related work on timed automata with a focus on semantical and algorithmic aspects of verification tools. We present the concrete and abstract semantics of timed automata (based on transition rules, regions and zones), decision problems, and algorithms for verification. A detailed description on DBM (Difference Bound Matrices) is included, which is the central data structure behind several verification tools for timed systems. As an example, we give a brief introduction to the tool Uppaal.},
  isbn = {978-3-540-27755-2},
  langid = {english}
}

@book{cassandrasIntroductionDiscreteEvent2021,
  title = {Introduction to {{Discrete Event Systems}}},
  author = {Cassandras, Christos G. and Lafortune, St{\'e}phane},
  year = {2021},
  month = nov,
  edition = {3},
  publisher = {Springer},
  address = {Cham},
  url = {https://doi.org/10.1007/978-3-030-72274-6},
  isbn = {978-3-030-72272-2},
  langid = {english}
}

@unpublished{esparzaAutomataTheoryAlgorithmic2017,
  type = {Lecture Notes for a Course on Finite and Omega-Automata},
  title = {Automata {{Theory}}: {{An Algorithmic Approach}}},
  author = {Esparza, Javier},
  year = {2017},
  month = aug,
  url = {https://www7.in.tum.de/~esparza/automatanotes.html},
  urldate = {2023-07-30},
  abstract = {These notes introduce the theory of finite- and omega-automata from an algorithmic point of view. Courses on data structures teach how to represent sets in a computer so that operations like insertion, deletion, or lookup, can be efficiently implemented. These notes present automata as a data structure for sets that allows for efficient implementations of the basic set-theoretical operations (union, intersection, and complement), decision procedures for basic properties (emptiness, universality, containment), and basic operations on relations (projection, join). Applications to pattern matching, formal verification, and decision procedures for logical and arithmetical theories are discussed.}
}

@book{esparzaAutomataTheoryAlgorithmic2023,
  title = {Automata {{Theory}}: {{An Algorithmic Approach}}},
  author = {Esparza, Javier and Blonding, Michael},
  year = {2023},
  month = oct,
  publisher = {The MIT Press},
  url = {https://mitpress.mit.edu/9780262048637/automata-theory/},
  urldate = {2023-07-30},
  abstract = {A comprehensive introduction to automata theory that uses the novel approach of viewing automata as data structures. This textbook presents automata theory from a fresh viewpoint inspired by its main modern application, program verification, where automata are viewed as data structures for the algorithmic manipulation of sets and relations. This novel ``automata as data structures'' paradigm makes holistic connections between automata theory and other areas of computer science not covered in traditional texts, linking the study of algorithms and data structures with that of the theory of formal languages and computability. Esparza and Blondin provide incisive overviews of core concepts along with illustrated examples and exercises that facilitate quick comprehension of rigorous material. {$\bullet$} Uses novel ``automata as data structures'' approach {$\bullet$} Algorithm approach ideal for programmers looking to broaden their skill set and researchers in automata theory and formal verification {$\bullet$} The first introduction to automata on infinite words that does not assume prior knowledge of finite automata {$\bullet$} Suitable for both undergraduate and graduate students {$\bullet$} Thorough, engaging presentation of concepts balances description, examples, and theoretical results  {$\bullet$} Extensive illustrations, exercises, and solutions deepen comprehension},
  isbn = {978-0-262-04863-7},
  langid = {american}
}

@book{harchol-balterPerformanceModelingDesign2013,
  title = {Performance {{Modeling}} and {{Design}} of {{Computer Systems}}: {{Queueing Theory}} in {{Action}}},
  shorttitle = {Performance {{Modeling}} and {{Design}} of {{Computer Systems}}},
  author = {{Harchol-Balter}, Mor},
  year = {18 {\'u}nora 2013},
  publisher = {Cambridge University Press},
  address = {Cambridge},
  url = {https://www.cs.cmu.edu/~harchol/PerformanceModeling/book.html},
  abstract = {Tackling the questions that systems designers care about, this book brings queueing theory decisively back to computer science. The book is written with computer scientists and engineers in mind and is full of examples from computer systems, as well as manufacturing and operations research. Fun and readable, the book is highly approachable, even for undergraduates, while still being thoroughly rigorous and also covering a much wider span of topics than many queueing books. Readers benefit from a lively mix of motivation and intuition, with illustrations, examples and more than 300 exercises -- all while acquiring the skills needed to model, analyze and design large-scale systems with good performance and low cost. The exercises are an important feature, teaching research-level counterintuitive lessons in the design of computer systems. The goal is to train readers not only to customize existing analyses but also to invent their own.},
  isbn = {978-1-107-02750-3}
}

@article{heymannConcurrencyDiscreteEvent1990,
  title = {Concurrency and Discrete Event Control},
  author = {Heymann, M.},
  year = {1990},
  month = jun,
  journal = {IEEE Control Systems Magazine},
  volume = {10},
  number = {4},
  pages = {103--112},
  issn = {2374-9385},
  doi = {10.1109/37.56284},
  abstract = {Much of discrete event control theory has been developed within the framework of automata and formal languages. An alternative approach inspired by the theories of process-algebra as developed in the computer science literature is presented. The framework, which rests on a new formalism of concurrency, can adequately handle nondeterminism and can be used for analysis of a wide range of discrete event phenomena.}
}

@article{lafortuneDiscreteEventSystems2019,
  title = {Discrete {{Event Systems}}: {{Modeling}}, {{Observation}}, and {{Control}}},
  shorttitle = {Discrete {{Event Systems}}},
  author = {Lafortune, St{\'e}phane},
  year = {2019},
  journal = {Annual Review of Control, Robotics, and Autonomous Systems},
  volume = {2},
  number = {1},
  pages = {141--159},
  doi = {10.1146/annurev-control-053018-023659},
  url = {https://doi.org/10.1146/annurev-control-053018-023659},
  urldate = {2022-09-20},
  abstract = {This article begins with an introduction to the modeling of discrete event systems, a class of dynamical systems with discrete states and event-driven dynamics. It then focuses on logical discrete event models, primarily automata, and reviews observation and control problems and their solution methodologies. Specifically, it discusses diagnosability and opacity in the context of partially observed discrete event systems. It then discusses supervisory control for both fully and partially observed systems. The emphasis is on presenting fundamental results first, followed by a discussion of current research directions.}
}

@article{lynchIntroductionInputOutput1989,
  title = {An Introduction to Input/Output Automata},
  author = {Lynch, Nancy and Tuttle, M. R.},
  year = {1989},
  month = sep,
  journal = {CWI Quarterly},
  volume = {2},
  number = {3},
  pages = {219--246},
  issn = {0922-5366},
  url = {https://ir.cwi.nl/pub/18164},
  urldate = {2022-09-21},
  langid = {english}
}

@article{ramadgeControlDiscreteEvent1989,
  title = {The Control of Discrete Event Systems},
  author = {Ramadge, P.J.G. and Wonham, W.M.},
  year = {1989},
  month = jan,
  journal = {Proceedings of the IEEE},
  volume = {77},
  number = {1},
  pages = {81--98},
  issn = {1558-2256},
  doi = {10.1109/5.21072},
  abstract = {A discrete event system (DES) is a dynamic system that evolves in accordance with the abrupt occurrence, at possibly unknown irregular intervals, of physical events. Such systems arise in a variety of contexts ranging from computer operating systems to the control of complex multimode processes. A control theory for the logical aspects of such DESs is surveyed. The focus is on the qualitative aspects of control, but computation and the related issue of computational complexity are also considered. Automata and formal language models for DESs are surveyed.}
}

@article{schafaschekOptimalControlTimed2020,
  title = {Optimal Control of Timed Event Graphs with Resource Sharing and Output-Reference Update},
  author = {Schafaschek, Germano and Hardouin, Laurent and Raisch, J{\"o}rg},
  year = {2020},
  month = jul,
  journal = {at - Automatisierungstechnik},
  volume = {68},
  number = {7},
  pages = {512--528},
  publisher = {De Gruyter (O)},
  issn = {2196-677X},
  doi = {10.1515/auto-2020-0051},
  url = {https://www.degruyter.com/document/doi/10.1515/auto-2020-0051/html},
  urldate = {2022-10-06},
  abstract = {Timed event graphs (TEGs) are a subclass of timed Petri nets that model synchronization and delay phenomena, but not conflict or choice. We consider a scenario where a number of TEGs share one or several resources and are subject to changes in their output-reference signals. Because of resource sharing, the resulting overall discrete event system is not a TEG. We propose a formal method to determine the optimal control input for such systems, where optimality is in the sense of the widely adopted just-in-time criterion. Our approach is based on a prespecified priority policy for the TEG components of the overall system. It builds on existing control theory for TEGs, which exploits the fact that, in a suitable mathematical framework (idempotent semirings such as the max-plus or the min-plus algebra), the temporal evolution of TEGs can be described by a set of linear time-invariant equations.},
  langid = {english}
}

@misc{SimEventsGettingStarted2022,
  title = {{{SimEvents Getting Started Guide}}},
  year = {2022},
  url = {https://www.mathworks.com/help/pdf_doc/simevents/simevents_gs.pdf},
  howpublished = {The Mathworks}
}

@misc{SimEventsUserGuide2022,
  title = {{{SimEvents User}}'s {{Guide}}},
  year = {2022},
  url = {https://www.mathworks.com/help/pdf_doc/simevents/simevents.pdf},
  howpublished = {The Mathworks}
}

@misc{topcuLectureAutomataTheory2013,
  type = {Lecture Slides},
  title = {Lecture 2 {{Automata Theory}}, Course on {{Specification}}, {{Design}}, and {{Verification}} of {{Networked Control Systems}}},
  author = {Topcu, Ufuk and Wongpiromsarn, Nok and Murray, Richard M.},
  year = {2013},
  month = mar,
  address = {Belgrade, Serbia},
  url = {http://www.cds.caltech.edu/~murray/courses/eeci-sp13/L2_automata-18Mar13.pdf},
  langid = {english}
}

@article{wonhamSupervisoryControlDiscreteevent2018,
  title = {Supervisory Control of Discrete-Event Systems: {{A}} Brief History},
  shorttitle = {Supervisory Control of Discrete-Event Systems},
  author = {Wonham, W. M. and Cai, Kai and Rudie, Karen},
  year = {2018},
  month = jan,
  journal = {Annual Reviews in Control},
  volume = {45},
  pages = {250--256},
  issn = {1367-5788},
  doi = {10.1016/j.arcontrol.2018.03.002},
  url = {https://www.sciencedirect.com/science/article/pii/S1367578817301876},
  urldate = {2022-09-16},
  abstract = {This brief history summarizes the `supervisory control of discrete-event systems' as it has evolved in the period 1980--2017. Overall, the trend has been from centralized or `monolithic' control to more structured architectures, and from `naive' to symbolic computation. Like any `history' this one represents the perspective of the authors; in consequence some important contributions may have been overlooked or short-changed.},
  langid = {english}
}

@book{wonhamSupervisoryControlDiscreteEvent2019,
  title = {Supervisory {{Control}} of {{Discrete-Event Systems}}},
  author = {Wonham, W. Murray and Cai, Kai},
  year = {2019},
  series = {Communications and {{Control Engineering}}},
  publisher = {Springer},
  address = {Cham},
  url = {https://doi.org/10.1007/978-3-319-77452-7},
  isbn = {978-3-319-77451-0},
  langid = {english}
}

@article{xuOptimisticOptimizationModel2016,
  title = {Optimistic Optimization for Model Predictive Control of Max-plus Linear Systems},
  author = {Xu, Jia and {van den Boom}, Ton and De Schutter, Bart},
  year = {2016},
  month = dec,
  journal = {Automatica},
  volume = {74},
  pages = {16--22},
  issn = {0005-1098},
  doi = {10.1016/j.automatica.2016.07.002},
  url = {https://www.sciencedirect.com/science/article/pii/S0005109816302709},
  urldate = {2022-10-06},
  abstract = {Model predictive control for max-plus linear discrete-event systems usually leads to a nonsmooth nonconvex optimization problem with real valued variables, which may be hard to solve efficiently. An alternative approach is to transform the given problem into a mixed integer linear programming problem. However, the computational complexity of current mixed integer linear programming algorithms increases in the worst case exponentially as a function of the prediction horizon. The focus of this paper is on making optimistic optimization suited to solve the given problem. Optimistic optimization is a class of algorithms that can find an approximation of the global optimum for general nonlinear optimization. A key advantage of optimistic optimization is that one can specify the computational budget in advance and guarantee bounds on the suboptimality with respect to the global optimum. We prove that optimistic optimization can be applied for the given problem by developing a dedicated semi-metric and by proving it satisfies the necessary requirements for optimistic optimization. Moreover, we show that the complexity of optimistic optimization is exponential in the control horizon instead of the prediction horizon. Hence, using optimistic optimization is more efficient when the control horizon is small and the prediction horizon is large.},
  langid = {english}
}

@book{zimmermannStochasticDiscreteEvent2008,
  title = {Stochastic {{Discrete Event Systems}}: {{Modeling}}, {{Evaluation}}, {{Applications}}},
  shorttitle = {Stochastic {{Discrete Event Systems}}},
  author = {Zimmermann, Armin},
  year = {2008},
  publisher = {Springer},
  address = {Berlin; Heidelberg},
  url = {https://doi.org/10.1007/978-3-540-74173-2},
  abstract = {Stochastic discrete-event systems (SDES) capture the randomness in choices due to activity delays and the probabilities of decisions. This book delivers a comprehensive overview on modeling with a quantitative evaluation of SDES. It presents an abstract model class for SDES as a pivotal unifying result and details important model classes. The book also includes nontrivial examples to explain real-world applications of SDES.},
  isbn = {978-3-540-74172-5},
  langid = {english}
}