@techreport{NUREG-0899,
  title       = {Guidelines for the Preparation of Emergency Operating Procedures},
  author      = {{U.S. Nuclear Regulatory Commission}},
  institution = {U.S. Nuclear Regulatory Commission},
  year        = {1982},
  number      = {NUREG-0899}
}

@misc{10CFR50.34,
  title        = {{10 CFR Part 50.34}},
  author       = {{U.S. Nuclear Regulatory Commission}},
  howpublished = {Code of Federal Regulations},
  urlyear = {2025},
	month = dec,
  url          = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0034}
}

@misc{10CFR55.59,
  title = {{10 CFR Part 55.59}},
  author       = {{U.S. Nuclear Regulatory Commission}},
  howpublished = {Code of Federal Regulations},
  urlyear = {2025},
	month = dec,
  url          = {https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/part055-0059}
}

@misc{10CFR55,
	title = {{Part 55—Operators' Licenses}},
	author = {{U.S. Nuclear Regulatory Commission}},
	howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part055/full-text}},
}

@misc{10CFR50.54,
	title = {{§ 50.54 Conditions of Licenses}},
  author = {{U.S. Nuclear Regulatory Commission}},
	howpublished = {\url{https://www.nrc.gov/reading-rm/doc-collections/cfr/part050/part050-0054}},
	urlyear = {2025},
	month = nov,
}

@techreport{WRPS.Description,
    author = {{Westinghouse Electric Corporation}},
    title = {{Westinghouse RPS System Description}},
    institution = {Westinghouse Electric Corporation},
    url = {https://nrcoe.inl.gov/publicdocs/SystemStudies/rps-w-description.pdf},
    urlyear = {2025},
	month = dec
}

@misc{gentillon_westinghouse_1999,
	title = {Westinghouse Reactor Protection System Unavailability, 1984-1995},
	url = {https://digital.library.unt.edu/ark:/67531/metadc620476/},
	note = {{PSA} '99, Washington, {DC} ({US}), 08/22/1999--08/25/1999},
	type = {Article},
	author = {Gentillon, C. D. and Marksberry, D. and Rasmuson, D. and Calley, M. B. and Eide, S. A. and Wierman, T.},
	urlyear = {2025},
	month = dec,
	year = {1999},
	month = aug,
	note = {Number: {INEEL}/{CON}-99-00374
Publisher: Idaho National Engineering and Environmental Laboratory},
}

@misc{operator_statistics,
	title = {{Operator Licensing}},
  author       = {{U.S. Nuclear Regulatory Commission}},
  howpublished = {\url{https://www.nrc.gov/reactors/operator-licensing}},
	urlyear = {2025},
	month = nov,
}

@techreport{Kemeny1979,
  title       = {Report of the President's Commission on the Accident at Three Mile Island},
  author      = {Kemeny, John G. and others},
  institution = {President's Commission on the Accident at Three Mile Island},
  year        = {1979},
  month       = {October}
}

@article{noauthor_human_nodate,
	title = {Human {Performance} {Improvement} {Handbook}, {Volume} 1},
	language = {en},
	file = {PDF:/Users/danesabo/Zotero/storage/HQZTH3YI/Human Performance Improvement Handbook, Volume 1.pdf:application/pdf},
}

@misc{WNA2020,
  title        = {Safety of Nuclear Power Reactors},
  author       = {{World Nuclear Association}},
  year         = {2020},
  howpublished = {\url{https://www.world-nuclear.org/information-library/safety-and-security/safety-of-plants/safety-of-nuclear-power-reactors.aspx}}
}

@article{hogberg_root_2013,
	title = {Root Causes and Impacts of Severe Accidents at Large Nuclear Power Plants},
	volume = {42},
	issn = {0044-7447},
	url = {https://pmc.ncbi.nlm.nih.gov/articles/PMC3606704/},
	doi = {10.1007/s13280-013-0382-x},
	pages = {267--284},
	number = {3},
	journal = {Ambio},
	author = {Högberg, Lars},
	urlyear = {2025},
	month = dec,
	year = {2013},
	month = apr,
	pmid = {23423737},
	pmcid = {PMC3606704},
}

@article{zhang_analysis_2025,
	title = {Analysis of human errors in nuclear power plant event reports},
	volume = {57},
	issn = {1738-5733},
	url = {https://www.sciencedirect.com/science/article/pii/S1738573325002554},
	doi = {10.1016/j.net.2025.103687},
	pages = {103687},
	number = {10},
	journal = {Nuclear Engineering and Technology},
	author = {Zhang, Meihui and Dai, Licao and Chen, Wenming and Pang, Ensheng},
	urlyear = {2025},
	month = dec,
	year = {2025},
	month = oct,
	keywords = {Active errors, {HFACS} model, Latent errors, Licensee event reports},
}

@techreport{Kiniry2024,
  title       = {High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) Final Technical Report},
  author      = {Kiniry, Joseph and Bakst, Alexander and Hansen, Simon and Podhradsky, Michal and Bivin, Andrew},
  institution = {Galois, Inc. / U.S. Nuclear Regulatory Commission},
  year        = {2024},
  number      = {TLR-RES-RES/DE-2024-005},
  note        = {NRC Contract 31310021C0014}
}

@techreport{eia_lcoe_2022,
  author       = {{U.S. Energy Information Administration}},
  title        = {Levelized Costs of New Generation Resources in the Annual Energy Outlook 2022},
  institution  = {U.S. Energy Information Administration},
  year         = {2022},
  month        = {March},
  type         = {Report},
  url          = {https://www.eia.gov/outlooks/aeo/pdf/electricity_generation.pdf},
  note         = {See Table 1b, page 9}
}

@misc{eesi_datacenter_2024,
  author       = {{Environmental and Energy Study Institute}},
  title        = {Data Center Energy Needs Are Upending Power Grids and Threatening the Climate},
  howpublished = {Web article},
  year         = {2024},
  url          = {https://www.eesi.org/articles/view/data-center-energy-needs-are-upending-power-grids-and-threatening-the-climate},
  note         = {Accessed: 2025-09-29}
}

@book{baier_principles_2008,
	address = {Cambridge, {MA}, {USA}},
	title = {Principles of Model Checking},
	isbn = {978-0-262-02649-9},
	abstract = {A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises.},
	publisher = {{MIT} Press},
	author = {Baier, Christel and Katoen, Joost-Pieter},
	year = {2008},
	month = apr,
}

@article{platzer_differential_2008,
	title = {Differential {Dynamic} {Logic} for {Hybrid} {Systems}},
	volume = {41},
	issn = {1573-0670},
	url = {https://doi.org/10.1007/s10817-008-9103-8},
	doi = {10.1007/s10817-008-9103-8},
	abstract = {Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics.},
	language = {en},
	number = {2},
	urlyear = {2025},
	month = sep,
	journal = {Journal of Automated Reasoning},
	author = {Platzer, André},
	month = aug,
	year = {2008},
	keywords = {Automated theorem proving, Axiomatisation, Differential equations, Dynamic logic, Sequent calculus, Verification of hybrid systems},
	pages = {143--189},
}

@inproceedings{fulton_keymaera_2015,
	address = {Cham},
	title = {{KeYmaera} {X}: {An} {Axiomatic} {Tactical} {Theorem} {Prover} for {Hybrid} {Systems}},
	isbn = {978-3-319-21401-6},
	shorttitle = {{KeYmaera} {X}},
	doi = {10.1007/978-3-319-21401-6_36},
	abstract = {KeYmaera X is a theorem prover for differential dynamic logic (), a logic for specifying and verifying properties of hybrid systems. Reasoning about complicated hybrid systems models requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute these tactics in parallel, and interface with partial proofs via an extensible user interface.},
	language = {en},
	booktitle = {Automated {Deduction} - {CADE}-25},
	publisher = {Springer International Publishing},
	author = {Fulton, Nathan and Mitsch, Stefan and Quesel, Jan-David and Völp, Marcus and Platzer, André},
	editor = {Felty, Amy P. and Middeldorp, Aart},
	year = {2015},
	keywords = {Adaptive Cruise Control, Hybrid automaton, Proof Rule, Proof Tree, Sequent calculus},
	pages = {527--538},
}

@inproceedings{alur_hybrid_1993,
	address = {Berlin, Heidelberg},
	title = {Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems},
	isbn = {978-3-540-48060-0},
	doi = {10.1007/3-540-57318-6_30},
	shorttitle = {Hybrid automata},
	pages = {209--229},
	booktitle = {Hybrid Systems},
	publisher = {Springer},
	author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A. and Ho, Pei -Hsin},
	editor = {Grossman, Robert L. and Nerode, Anil and Ravn, Anders P. and Rischel, Hans},
	year = {1993},
	keywords = {Acceptance Condition, Hybrid Automaton, Hybrid System, Mutual Exclusion, Reachability Problem},
}

@techreport{katis_realizability_2022,
	title = {Realizability {Checking} of {Requirements} in {FRET}},
	url = {https://ntrs.nasa.gov/citations/20220007510},
	abstract = {Requirements formalization has become increasingly popular in industrial settings as an
effort to disambiguate designs and optimize development time and costs for critical system components. Formal requirements elicitation also enables the employment of analysis
tools to prove important properties, such as consistency and realizability. In this report,
we present the realizability analysis framework that we developed as part of the Formal
Requirements Elicitation Tool (FRET). Our framework prioritizes usability, and employs
state-of-the-art analysis algorithms that support infinite theories. We demonstrate the workflow for realizability checking, showcase the diagnosis process that supports visualization of
conflicts between requirements and simulation of counterexamples, and discuss results from
industrial-level case studies.},
	urlyear = {2026},
	month = mar,
	institution = {NASA Ames Research Center},
	author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann},
	month = apr,
	year = {2022},
	note = {NTRS Author Affiliations: Wyle (United States), Ames Research Center
NTRS Document ID: 20220007510
NTRS Research Center: Ames Research Center (ARC)},
	keywords = {Mathematical And Computer Sciences (General)},
}

@inproceedings{katis_capture_2022,
	address = {Cham},
	title = {Capture, Analyze, Diagnose: Realizability Checking Of Requirements in {FRET}},
	isbn = {978-3-031-13188-2},
	doi = {10.1007/978-3-031-13188-2_24},
	shorttitle = {Capture, Analyze, Diagnose},
	pages = {490--504},
	booktitle = {Computer Aided Verification},
	publisher = {Springer International Publishing},
	author = {Katis, Andreas and Mavridou, Anastasia and Giannakopoulou, Dimitra and Pressburger, Thomas and Schumann, Johann},
	editor = {Shoham, Sharon and Vizel, Yakir},
	year = {2022},
}

@techreport{pressburger_using_2023,
	title = {Using {FRET} to {Create}, {Analyze} and {Monitor} {Requirements} for a {Lift} {Plus} {Cruise} {Case} {Study}},
	url = {https://ntrs.nasa.gov/citations/20220017032},
	abstract = {In this technical report we provide information on the use of the NASA Formal RequirementsElicitation Tool (FRET) to create requirements for a Lift Plus Cruise (LPC) aircraft case study.  Furthermore, we provide details on using FRET to translate these requirements into an appropriate format for the Copilot tool, enabling their usage to perform runtime verification on a synthesized LPC system.},
	urlyear = {2026},
	month = mar,
	institution = {NASA Ames Research Center},
	author = {Pressburger, Thomas and Katis, Andreas and Dutle, Aaron and Mavridou, Anastasia},
	month = apr,
	year = {2023},
	note = {NTRS Author Affiliations: Ames Research Center, KBR (United States), Langley Research Center
NTRS Document ID: 20220017032
NTRS Research Center: Ames Research Center (ARC)},
	keywords = {Mathematical And Computer Sciences (General)},
}

@inproceedings{meyer_strix_2018,
	address = {Cham},
	title = {Strix: Explicit Reactive Synthesis Strikes Back!},
	isbn = {978-3-319-96145-3},
	doi = {10.1007/978-3-319-96145-3_31},
	shorttitle = {Strix},
	pages = {578--586},
	booktitle = {Computer Aided Verification},
	publisher = {Springer International Publishing},
	author = {Meyer, Philipp J. and Sickert, Salomon and Luttenberger, Michael},
	editor = {Chockler, Hana and Weissenbacher, Georg},
	year = {2018},
}

@misc{jacobs_reactive_2024,
	title = {The Reactive Synthesis Competition ({SYNTCOMP}): 2018-2021},
	url = {http://arxiv.org/abs/2206.00251},
	doi = {10.48550/arXiv.2206.00251},
	shorttitle = {The Reactive Synthesis Competition ({SYNTCOMP})},
	number = {{arXiv}:2206.00251},
	publisher = {{arXiv}},
	author = {Jacobs, Swen and others},
	urlyear = {2025},
	month = dec,
	year = {2024},
	month = may,
	keywords = {Computer Science - Logic in Computer Science},
}

@book{lunze_handbook_2009,
	address = {Cambridge},
	title = {Handbook of {Hybrid} {Systems} {Control}: {Theory}, {Tools}, {Applications}},
	isbn = {978-0-521-76505-3},
	shorttitle = {Handbook of {Hybrid} {Systems} {Control}},
	url = {https://www.cambridge.org/core/books/handbook-of-hybrid-systems-control/95CBB51B339FA6B95B814D4BABB715A7},
	doi = {10.1017/CBO9780511807930},
	abstract = {Setting out core theory and reviewing a range of new methods, theoretical problems and applications, this handbook shows how hybrid dynamical systems can be modelled and understood. Sixty expert authors involved in the recent research activities and industrial application studies provide practical insights on topics ranging from the theoretical investigations over computer-aided design to applications in energy management and the process industry. Structured into three parts, the book opens with a thorough introduction to hybrid systems theory, illustrating new dynamical phenomena through numerous examples. Part II then provides a survey of key tools and tool integration activities. Finally, Part III is dedicated to applications, implementation issues and system integration, considering different domains such as industrial control, automotive systems and digital networks. Three running examples are referred to throughout the book, together with numerous illustrations, helping both researchers and industry professionals to understand complex theory, recognise problems and find appropriate solutions.},
	urlyear = {2026},
	month = jan,
	publisher = {Cambridge University Press},
	editor = {Lunze, Jan and Lamnabhi-Lagarrigue, Françoise},
	year = {2009},
}

@article{branicky_multiple_1998,
	title = {Multiple Lyapunov functions and other analysis tools for switched and hybrid systems},
	volume = {43},
	issn = {1558-2523},
	url = {https://ieeexplore.ieee.org/document/664150},
	doi = {10.1109/9.664150},
	pages = {475--482},
	number = {4},
	journal = {{IEEE} Transactions on Automatic Control},
	author = {Branicky, M.S.},
	urlyear = {2025},
	month = sep,
	year = {1998},
	month = apr,
	keywords = {Automata, Control systems, Difference equations, Differential equations, Lagrangian functions, Limit-cycles, Lyapunov method, Stability analysis, Switched systems, Switches},
}

@phdthesis{kapuria_using_2025,
	address = {United States -- Pennsylvania},
	type = {Ph.{D}.},
	title = {Using {Decomposition}-{Based} {Formal} {Verification} to {Analyze} {Safety} and {Identify} {Unsafe} {Control} {Actions} for {Hybrid} {Systems}},
	copyright = {Database copyright ProQuest LLC; ProQuest does not claim copyright in the individual underlying works.},
	isbn = {9798280700147},
	url = {https://www.proquest.com/docview/3215670525/abstract/3C715CB23CB84313PQ/1},
	abstract = {This dissertation presents a decomposition-based formal verification framework for hybrid systems, focusing on identifying unsafe control actions (UCAs) in cyber-physical systems (CPS). Using differential dynamic logic, we verify safety properties by first proving correctness at the component level before integrating them into a system-wide proof. Our approach enhances scalability by isolating subsystems, enforcing constraints on their interactions, and using satisfiability modulo theories (SMT) solvers to automate invariant generation. We apply this methodology to a small modular advanced high-temperature reactor (SmAHTR), analyzing its control logic under both normal operations and adversarial conditions, including cyberattacks. The results demonstrate how formal methods can systematically identify UCAs that emerge from mode transitions, feedback interactions, and incorrect assumptions. By integrating theorem proving with reachability analysis, this work advances CPS safety verification, providing a rigorous and scalable approach to ensuring system resilience.
To achieve this, we develop a hybrid automaton model of SmAHTR and formally verify its behavior under various control strategies, including scenarios involving maintenance operations and external disruptions. We introduce a structured method to decompose the system into independently analyzable components, ensuring that local safety guarantees extend to global system correctness. The verification process captures both intended and unintended control actions, revealing potential failure modes that traditional analysis methods might overlook. Furthermore, we propose an automated approach for identifying UCAs by leveraging formal reasoning tools to systematically explore system behaviors beyond manual hazard analysis. Our findings demonstrate that decomposition-based verification not only reduces computational complexity but also improves the efficiency and robustness of CPS safety analysis, particularly for high-assurance applications such as nuclear reactor operations.},
	language = {English},
	urlyear = {2026},
	month = feb,
	school = {University of Pittsburgh},
	author = {Kapuria, Abhimanyu},
	year = {2025},
	keywords = {Computer science, Differential equations, Electrical engineering, Engineering, Formal verification, Hybrid systems, Mechanical engineering, Reachability analysis, Satisfiability modulo theories solvers},
}

@inproceedings{lang_formal_2021,
	address = {VIRTUAL EVENT},
	title = {Formal {Verification} {Applied} to {Spacecraft} {Attitude} {Control}},
	isbn = {978-1-62410-609-5},
	url = {https://arc.aiaa.org/doi/10.2514/6.2021-1126},
	doi = {10.2514/6.2021-1126},
	language = {en},
	urlyear = {2024},
	month = nov,
	booktitle = {{AIAA} {Scitech} 2021 {Forum}},
	publisher = {American Institute of Aeronautics and Astronautics},
	author = {Lang, Kendra and Klett, Corbin and Hawkins, Kelsey and Feron, Eric and Tsiotras, Panagiotis and Phillips, Sean},
	month = jan,
	year = {2021},
}

@inproceedings{frehse_spaceex_2011,
	address = {Berlin, Heidelberg},
	title = {{SpaceEx}: Scalable Verification of Hybrid Systems},
	isbn = {978-3-642-22110-1},
	doi = {10.1007/978-3-642-22110-1_30},
	shorttitle = {{SpaceEx}},
	pages = {379--395},
	booktitle = {Computer Aided Verification},
	publisher = {Springer},
	author = {Frehse, Goran and Le Guernic, Colas and Donzé, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
	editor = {Gopalakrishnan, Ganesh and Qadeer, Shaz},
	year = {2011},
	keywords = {Hybrid Automaton, Hybrid System, Reachability Analysis, Reachable State, Support Function},
}

@phdthesis{guernic_reachability_2009,
	title = {Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics},
	url = {https://theses.hal.science/tel-00422569},
	institution = {Université Joseph-Fourier - Grenoble I},
	school = {Université Joseph-Fourier, Grenoble},
	author = {Guernic, Colas Le},
	urlyear = {2025},
	month = sep,
	year = {2009},
	month = oct,
}

@article{mitchell_time-dependent_2005,
	title = {A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games},
	volume = {50},
	issn = {1558-2523},
	url = {https://ieeexplore.ieee.org/abstract/document/1463302},
	doi = {10.1109/TAC.2005.851439},
	pages = {947--957},
	number = {7},
	journal = {{IEEE} Transactions on Automatic Control},
	author = {Mitchell, I.M. and Bayen, A.M. and Tomlin, C.J.},
	urlyear = {2025},
	month = sep,
	year = {2005},
	month = jul,
	keywords = {Aircraft, Collaborative software, Collision avoidance, Computational modeling, Differential games, Hamilton–Jacobi equations, Nonlinear equations, Nonlinear systems, Partial differential equations, reachability, Trajectory, Vehicle dynamics, verification, Viscosity},
}

@inproceedings{bansal_hamilton-jacobi_2017,
	title = {Hamilton-Jacobi reachability: A brief overview and recent advances},
	url = {https://ieeexplore.ieee.org/abstract/document/8263977},
	doi = {10.1109/CDC.2017.8263977},
	shorttitle = {Hamilton-Jacobi reachability},
	eventtitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})},
	pages = {2242--2253},
	booktitle = {2017 {IEEE} 56th Annual Conference on Decision and Control ({CDC})},
	author = {Bansal, Somil and Chen, Mo and Herbert, Sylvia and Tomlin, Claire J.},
	urlyear = {2025},
	month = sep,
	year = {2017},
	month = dec,
	keywords = {Aircraft, Games, Level set, Safety, Tools, Trajectory, Tutorials},
}

@inproceedings{prajna_safety_2004,
	address = {Berlin, Heidelberg},
	title = {Safety Verification of Hybrid Systems Using Barrier Certificates},
	isbn = {978-3-540-24743-2},
	doi = {10.1007/978-3-540-24743-2_32},
	pages = {477--492},
	booktitle = {Hybrid Systems: Computation and Control},
	publisher = {Springer},
	author = {Prajna, Stephen and Jadbabaie, Ali},
	editor = {Alur, Rajeev and Pappas, George J.},
	year = {2004},
	keywords = {Continuous State, Discrete Transition, Hybrid System, Integral Constraint, Reachability Analysis},
}

@techreport{deroucy_ai_2025,
  title       = {AI, Data Centers and Energy Demand: Reassessing and Exploring the Trends},
  author      = {de Roucy-Rochegonde, Laure and Buffard, Adrien},
  institution = {French Institute of International Relations (Ifri)},
  year        = {2025},
  type        = {Ifri Papers},
  isbn        = {979-10-373-1000-2}
}


@article{harvey_levels_2021,
	title = {The {Levels} of {War} as {Levels} of {Analysis}},
	language = {en},
	publisher = {Military Review},
	author = {Harvey, Andrew S},
	year = {2021},
	file = {PDF:/Users/danesabo/Zotero/storage/5NSKMNEU/Harvey - The Levels of War as Levels of Analysis.pdf:application/pdf},
}

@article{luttenberger_practical_2020,
	title = {Practical synthesis of reactive systems from {LTL} specifications via parity games},
	volume = {57},
	issn = {1432-0525},
	url = {https://doi.org/10.1007/s00236-019-00349-3},
	doi = {10.1007/s00236-019-00349-3},
	abstract = {The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.},
	language = {en},
	number = {1},
	urldate = {2026-03-07},
	journal = {Acta Informatica},
	author = {Luttenberger, Michael and Meyer, Philipp J. and Sickert, Salomon},
	month = apr,
	year = {2020},
	pages = {3--36},
	file = {Submitted Version:/Users/danesabo/Zotero/storage/VYMVF5GK/Luttenberger et al. - 2020 - Practical synthesis of reactive systems from LTL specifications via parity games.pdf:application/pdf},
}


@inproceedings{chen_taylor_2012,
	title = {Taylor {Model} {Flowpipe} {Construction} for {Non}-linear {Hybrid} {Systems}},
	issn = {1052-8725},
	url = {https://ieeexplore.ieee.org/document/6424802},
	doi = {10.1109/RTSS.2012.70},
	abstract = {We propose an approach for verifying non-linear hybrid systems using higher-order Taylor models that are a combination of bounded degree polynomials over the initial conditions and time, bloated by an interval. Taylor models are an effective means for computing rigorous bounds on the complex time trajectories of non-linear differential equations. As a result, Taylor models have been successfully used to verify properties of non-linear continuous systems. However, the handling of discrete (controller) transitions remains a challenging problem. In this paper, we provide techniques for handling the effect of discrete transitions on Taylor model flow pipe construction. We explore various solutions based on two ideas: domain contraction and range over-approximation. Instead of explicitly computing the intersection of a Taylor model with a guard set, domain contraction makes the domain of a Taylor model smaller by cutting away parts for which the intersection is empty. It is complemented by range over-approximation that translates Taylor models into commonly used representations such as template polyhedra or zonotopes, on which intersections with guard sets have been previously studied. We provide an implementation of the techniques described in the paper and evaluate the various design choices over a set of challenging benchmarks.},
	urldate = {2026-03-18},
	booktitle = {2012 {IEEE} 33rd {Real}-{Time} {Systems} {Symposium}},
	author = {Chen, Xin and Ábrahám, Erika and Sankaranarayanan, Sriram},
	month = dec,
	year = {2012},
	note = {ISSN: 1052-8725},
	keywords = {Approximation methods, Computational modeling, Mathematical model, Polynomials, Safety, Taylor series, Trajectory},
	pages = {183--192},
	file = {Snapshot:/Users/danesabo/Zotero/storage/7HBF3VMT/6424802.html:text/html},
}

@inproceedings{chen_flow_2013,
	address = {Berlin, Heidelberg},
	title = {Flow*: {An} {Analyzer} for {Non}-linear {Hybrid} {Systems}},
	isbn = {978-3-642-39799-8},
	shorttitle = {Flow*},
	doi = {10.1007/978-3-642-39799-8_18},
	abstract = {The tool Flow* performs Taylor model-based flowpipe construction for non-linear (polynomial) hybrid systems. Flow* combines well-known Taylor model arithmetic techniques for guaranteed approximations of the continuous dynamics in each mode with a combination of approaches for handling mode invariants and discrete transitions. Flow* supports a wide variety of optimizations including adaptive step sizes, adaptive selection of approximation orders and the heuristic selection of template directions for aggregating flowpipes. This paper describes Flow* and demonstrates its performance on a series of non-linear continuous and hybrid system benchmarks. Our comparisons show that Flow* is competitive with other tools.},
	language = {en},
	booktitle = {Computer {Aided} {Verification}},
	publisher = {Springer},
	author = {Chen, Xin and Ábrahám, Erika and Sankaranarayanan, Sriram},
	editor = {Sharygina, Natasha and Veith, Helmut},
	year = {2013},
	keywords = {Adaptive Step, Adaptive Step Size, Discrete Transition, Hybrid System, Taylor Model},
	pages = {258--263},
	file = {Full Text PDF:/Users/danesabo/Zotero/storage/6QV2XCVF/Chen et al. - 2013 - Flow An Analyzer for Non-linear Hybrid Systems.pdf:application/pdf},
}


@inproceedings{althoff_introduction_nodate,
	title = {An {Introduction} to {CORA} 2015},
	url = {https://easychair.org/publications/paper/xMm},
	doi = {10.29007/zbkv},
	abstract = {The philosophy, architecture, and capabilities of the COntinuous Reachability Analyzer (CORA) are presented. CORA is a toolbox that integrates various vector and matrix set representations and operations on them as well as reachability algorithms of various dynamic system classes. The software is designed such that set representations can be exchanged without having to modify the code for reachability analysis. CORA has a modular design, making it possible to use the capabilities of the various set representations for other purposes besides reachability analysis. The toolbox is designed using the object oriented paradigm, such that users can safely use methods without concerning themselves with detailed information hidden inside the object. Since the toolbox is written in MATLAB, the installation and use is platform independent.},
	urldate = {2026-03-18},
	author = {Althoff, Matthias},
	pages = {120--87},
	file = {Full Text:/Users/danesabo/Zotero/storage/BIGJMRCV/Althoff - An Introduction to CORA 2015.pdf:application/pdf},
}


@article{bogomolov_reachability_2020,
	title = {Reachability {Analysis} of {Linear} {Hybrid} {Systems} via {Block} {Decomposition}},
	volume = {39},
	issn = {1937-4151},
	url = {https://ieeexplore.ieee.org/document/9211556},
	doi = {10.1109/TCAD.2020.3012859},
	abstract = {Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this article, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.},
	number = {11},
	urldate = {2026-03-18},
	journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
	author = {Bogomolov, Sergiy and Forets, Marcelo and Frehse, Goran and Potomkin, Kostiantyn and Schilling, Christian},
	month = nov,
	year = {2020},
	keywords = {Approximation algorithms, Decomposition, Design automation, Heuristic algorithms, hybrid systems, Integrated circuits, Linear systems, reachability, Reachability analysis, Tools},
	pages = {4018--4029},
	file = {Snapshot:/Users/danesabo/Zotero/storage/D7FYXW7T/9211556.html:text/html;Submitted Version:/Users/danesabo/Zotero/storage/I3HNBQ65/Bogomolov et al. - 2020 - Reachability Analysis of Linear Hybrid Systems via Block Decomposition.pdf:application/pdf},
}