@article{15295,
  abstract     = {Background: Benzodiazepines and antidepressants are effective agents for the treatment of generalized anxiety disorder (GAD), with the HAM-A frequently used as a primary outcome measure. The GAD literature is inconsistent regarding which medications are more effective for somatic versus psychic symptoms of GAD, and treatment guidelines do not advocate for prescribing based on subtype. This meta-analysis aimed to determine whether benzodiazepines and antidepressants have a differential impact on the somatic versus psychic subscales of the HAM-A in GAD.

Methods: An electronic search was undertaken for randomized controlled trials of either benzodiazepines or antidepressants for GAD that reported treatment response using the HAM-A subscales. Data were extracted by independent reviewers. A random effects assessment of weighted mean difference with 95% confidence intervals and subgroup difference was applied. All analysis was done on SPSS 26. An assessment of bias, and of quality of evidence was performed.

Results: 24 randomized controlled trials met the inclusion criteria: 18 antidepressant trials, 5 benzodiazepine trials and 1 of both. 14 studies were assessed as having between some and high risk of bias, while 10 were assessed as having low risk of bias. Benzodiazepines (WMD of 1.81 [CI 1.03, 2.58]) were significantly more effective than antidepressants (WMD of 0.83 [CI 0.64, 1.02]) for reducing somatic symptoms of GAD (Chi2 = 5.81, p = 0.02), and were also more effective (WMD of 2.46 [CI 1.83, 3.09]) in reducing psychic symptoms than antidepressants (WMD of 1.83 [CI 1.55, 2.10]), although this comparison did not reach statistical significance (Chi2 = 3.31, p = 0.07).

Conclusion: The finding that benzodiazepines were significantly more effective than antidepressants for somatic symptoms needs to be weighed up against potential benefits of antidepressants over benzodiazepines. It may be useful for future treatment guidelines for GAD to explicitly consider symptom subtype.},
  author       = {Beyer, Chad and Currin, Christopher and Williams, Taryn and Stein, Dan J.},
  issn         = {1532-8384},
  journal      = {Comprehensive Psychiatry},
  publisher    = {Elsevier},
  title        = {{Meta-analysis of the comparative efficacy of benzodiazepines and antidepressants for psychic versus somatic symptoms of generalized anxiety disorder}},
  doi          = {10.1016/j.comppsych.2024.152479},
  volume       = {132},
  year         = {2024},
}

@inproceedings{17053,
  abstract     = {We introduce a formalization of ternary simulation as abstract interpretation along with a widening operator to speed up convergence. With the same goal, we present a subsumption algorithm that can determine termination earlier than the usual approach using hash sets. Additionally, we introduce a narrowing operator that utilizes recent advances in backbone extraction, allowing to increase the overapproximation precision in simulation at any time. The experiments evaluate the presented techniques in the context of hardware model checking.},
  author       = {Froleyks, Nils and Yu, Zhengqi and Biere, Armin},
  booktitle    = {27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems},
  isbn         = {9783800762682},
  location     = {Kaiserslautern, Germany},
  pages        = {148--151},
  publisher    = {VDE Verlag},
  title        = {{Ternary simulation as abstract interpretation (Work in Progress)}},
  year         = {2024},
}

@misc{23182,
  abstract     = {This online resource contains the simulation data and program codes required for reproducing all results of the study described in the article, and Supplementary Figures and Videos.},
  author       = {Zendrikov, Dmitrii and Paraskevov, Alexander},
  publisher    = {Figshare},
  title        = {{Supplementary Material for the article entitled "The vitals for steady nucleation maps of spontaneous spiking coherence in autonomous two-dimensional neuronal networks"}},
  doi          = {10.6084/m9.figshare.24527848},
  year         = {2024},
}

@inproceedings{18066,
  abstract     = {Graph games lie at the algorithmic core of many automated design problems in computer science. These are games usually played between two players on a given graph, where the players keep moving a token along the edges according to pre-determined rules (turn-based, concurrent, etc.), and the winner is decided based on the infinite path (aka play) traversed by the token from a given initial position. In bidding games, the players initially get some monetary budgets which they need to use to bid for the privilege of moving the token at each step. Each round of bidding affects the players' available budgets, which is the only form of update that the budgets experience. We introduce bidding games with charging where the players can additionally improve their budgets during the game by collecting vertex-dependent monetary rewards, aka the "charges." Unlike traditional bidding games (where all charges are zero), bidding games with charging allow non-trivial recurrent behaviors. For example, a reachability objective may require multiple detours to vertices with high charges to earn additional budget. We show that, nonetheless, the central property of traditional bidding games generalizes to bidding games with charging: For each vertex there exists a threshold ratio, which is the necessary and sufficient fraction of the total budget for winning the game from that vertex. While the thresholds of traditional bidding games correspond to unique fixed points of linear systems of equations, in games with charging, these fixed points are no longer unique. This significantly complicates the proof of existence and the algorithmic computation of thresholds for infinite-duration objectives. We also provide the lower complexity bounds for computing thresholds for Rabin and Streett objectives, which are the first known lower bounds in any form of bidding games (with or without charging), and we solve the following repair problem for safety and reachability games that have unsatisfiable objectives: Can we distribute a given amount of charge to the players in a way such that the objective can be satisfied?},
  author       = {Avni, Guy and Goharshady, Ehsan Kafshdar and Henzinger, Thomas A and Mallik, Kaushik},
  booktitle    = {35th International Conference on Concurrency Theory},
  isbn         = {9783959773393},
  issn         = {1868-8969},
  location     = {Calgary, Canada},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Bidding games with charging}},
  doi          = {10.4230/LIPIcs.CONCUR.2024.8},
  volume       = {311},
  year         = {2024},
}

@inproceedings{18067,
  abstract     = {An automaton 𝒜 is history-deterministic if its nondeterminism can be resolved on the fly, only using the prefix of the word read so far. This mild form of nondeterminism has attracted particular attention for its applications in synthesis problems. An automaton 𝒜 is guidable with respect to a class C of automata if it can fairly simulate every automaton in C, whose language is contained in that of 𝒜. In other words, guidable automata are those for which inclusion and simulation coincide, making them particularly interesting for model-checking. We study the connection between these two notions, and specifically the question of when they coincide. For classes of automata on which they do, deciding guidability, an otherwise challenging decision problem, reduces to deciding history-determinism, a problem that is starting to be well-understood for many classes. We provide a selection of sufficient criteria for a class of automata to guarantee the coincidence of the notions, and use them to show that the notions coincide for the most common automata classes, among which are ω-regular automata and many infinite-state automata with safety and reachability acceptance conditions, including vector addition systems with states, one-counter nets, pushdown-, Parikh-, and timed-automata. We also demonstrate that history-determinism and guidability do not always coincide, for example, for the classes of timed automata with a fixed number of clocks.},
  author       = {Boker, Udi and Henzinger, Thomas A and Lehtinen, Karoliina and Prakash, Aditya},
  booktitle    = {35th International Conference on Concurrency Theory},
  isbn         = {9783959773393},
  issn         = {1868-8969},
  location     = {Calgary, Canada},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{History-determinism vs fair simulation}},
  doi          = {10.4230/LIPIcs.CONCUR.2024.12},
  volume       = {311},
  year         = {2024},
}

@inproceedings{15376,
  abstract     = {Sequential decision-making tasks often require satisfaction of multiple, partially-contradictory objectives. Existing approaches are monolithic, where a single policy fulfills all objectives. We present auction-based scheduling, a decentralized framework for multi-objective sequential decision making. Each objective is fulfilled using a separate and independent policy. Composition of policies is performed at runtime, where at each step, the policies simultaneously bid from pre-allocated budgets for the privilege of choosing the next action. The framework allows policies to be independently created, modified, and replaced. We study path planning problems on finite graphs with two temporal objectives and present algorithms to synthesize policies together with bidding policies in a decentralized manner. We consider three categories of decentralized synthesis problems, parameterized by the assumptions that the policies make on each other. We identify a class of assumptions called assume-admissible for which synthesis is always possible for graphs whose every vertex has at most two outgoing edges.},
  author       = {Avni, Guy and Mallik, Kaushik and Sadhukhan, Suman},
  booktitle    = {30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031572555},
  issn         = {1611-3349},
  location     = {Luxembourg City, Luxembourg},
  pages        = {153--172},
  publisher    = {Springer Nature},
  title        = {{Auction-based scheduling}},
  doi          = {10.1007/978-3-031-57256-2_8},
  volume       = {14572},
  year         = {2024},
}

@inproceedings{17413,
  abstract     = {Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.},
  author       = {Froleyks, Nils and Yu, Zhengqi and Biere, Armin and Heljanko, Keijo},
  booktitle    = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
  isbn         = {9783031634970},
  issn         = {1611-3349},
  location     = {Nancy, France},
  pages        = {284--303},
  publisher    = {Springer Nature},
  title        = {{Certifying phase abstraction}},
  doi          = {10.1007/978-3-031-63498-7_17},
  volume       = {14739},
  year         = {2024},
}

@inproceedings{15333,
  abstract     = {BUBAAK-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top of BUBAAK, a tool designed for running combinations of verifiers in parallel. In contrast to BUBAAK, that directly invokes verifiers on the inputs, BUBAAK-SpLit first starts by splitting the input program into multiple modified versions called program splits. During the splitting process, BUBAAK-SpLit utilizes a weak verifier (in our case symbolic execution with a short timelimit) to analyze each generated program split. If the weak verifier fails on a program split, we split this program split again and start the verification process again on the generated program splits. We run the splitting process until a predefined number of hard-to-verify program splits is generated or a splitting limit is reached. During the main verification phase, we run a combination of BUBAAK-LEE and SLOWBEAST in parallel on the remaining unsolved parts of the verification task.},
  author       = {Chalupa, Marek and Richter, Cedric},
  booktitle    = {30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031572555},
  issn         = {1611-3349},
  location     = {Luxembourg City, Luxembourg},
  pages        = {353–358},
  publisher    = {Springer Nature},
  title        = {{Bubaak-SpLit: Split what you cannot verify (Competition contribution)}},
  doi          = {10.1007/978-3-031-57256-2_20},
  volume       = {14572},
  year         = {2024},
}

@inproceedings{15377,
  abstract     = {We provide an algorithmto solve Rabin and Streett games over graphs
with n vertices,m edges, and k colours that runs in ˜O³mn(k!)1+o(1)´time and
O(nk logk logn) space, where ˜O hides poly-logarithmic factors. Our algorithm
is an improvement by a super quadratic dependence on k! from the currently
best known run time of O³mn2(k!)2+o(1)´, obtained by converting a Rabin
gameinto a parity game,while simultaneously improving its exponential space
requirement.
Our main technical ingredient is a characterisation of progress measures for
Rabin games using colourful trees and a combinatorial construction of succinctlyrepresented,
universal colourful trees. Colourful universal trees are generalisations
of universal trees used by Jurdzi´nski and Lazi´c (2017) to solve parity
games, as well as of Rabin progress measures of Klarlund and Kozen (1991).
Our algorithm for Rabin games is a progress measure lifting algorithm where
the lifting is performed on succinct, colourful, universal trees.},
  author       = {Majumdar, Rupak and Sağlam, Irmak and Thejaswini, K. S.},
  booktitle    = {30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031572555},
  issn         = {1611-3349},
  pages        = {213--231},
  publisher    = {Springer Nature},
  title        = {{Rabin games and colourful universal trees}},
  doi          = {10.1007/978-3-031-57256-2_11},
  volume       = {14572},
  year         = {2024},
}

@inproceedings{17898,
  abstract     = {There is an ever-growing zoo of modern neural network models that can efficiently learn end-to-end control from visual observations. These advanced deep models, ranging from convolutional to Vision Transformers, from small to gigantic networks, have been extensively tested on offline image classification tasks. In this paper, we study these vision models with respect to the open-loop training to closed-loop generalization abilities, i.e., deployment realizes a causal feedback loop that is not present during training. This causality gap typically emerges in robotics applications such as autonomous driving, where a network is trained to imitate the control commands of a human. In this setting, two situations arise: 1) Closed-loop testing in-distribution, where the test environment shares properties with those of offline training data. 2) Closed-loop testing under distribution shifts and out-of-distribution. Contrary to recently reported results, we show that under proper training guidelines, all vision architectures perform indistinguishably well on in-distribution deployment, resolving the causality gap. In situation 2, We observe that scale is the strongest factor in improving closed-loop generalization regardless of the choice of the model architecture. Our results predict the trend that in the future we will see larger and larger models being used in offline-training-online-deployment imitation learning tasks in robotic applications.},
  author       = {Lechner, Mathias and Hasani, Ramin and Amini, Alexander and Wang, Tsun Hsuan and Henzinger, Thomas A and Rus, Daniela},
  booktitle    = {Proceedings of the 2024 IEEE International Conference on Robotics and Automation},
  isbn         = {9798350384574},
  issn         = {1050-4729},
  location     = {Yokohama, Japan},
  pages        = {2774--2782},
  publisher    = {IEEE},
  title        = {{Overparametrization helps offline-to-online generalization of closed-loop control from pixels}},
  doi          = {10.1109/ICRA57147.2024.10610284},
  year         = {2024},
}

@inproceedings{15321,
  abstract     = {Boolean Networks (BNs) are widely used as a modeling formalism in several domains, notably systems biology and computer science. A fundamental problem in BN analysis is the enumeration of trap spaces, which are hypercubes in the state space that cannot be escaped once entered. Several methods have been proposed for enumerating trap spaces, however they often suffer from scalability and efficiency issues, particularly for large and complex models. To our knowledge, the most efficient and recent methods for the trap space enumeration all rely on Answer Set Programming (ASP), which has been widely applied to the analysis of BNs. Motivated by these considerations, our work proposes a new method for enumerating trap spaces in BNs using ASP. We evaluate the method on a mix of 250+ real-world and 400+ randomly generated BNs, showing that it enables analysis of models beyond the capabilities of existing tools (namely pyboolnet, mpbn, trappist, and trapmvn).},
  author       = {Trinh, Giang and Benhamou, Belaid and Pastva, Samuel and Soliman, Sylvain},
  booktitle    = {Proceedings of the 38th AAAI Conference on Artificial Intelligence},
  isbn         = {1577358872},
  issn         = {2374-3468},
  number       = {9},
  pages        = {10714--10722},
  publisher    = {Association for the Advancement of Artificial Intelligence},
  title        = {{Scalable enumeration of trap spaces in boolean networks via answer set programming}},
  doi          = {10.1609/aaai.v38i9.28943},
  volume       = {38},
  year         = {2024},
}

@inproceedings{18521,
  abstract     = {In distributed systems with processes that do not share a global clock, partial synchrony is achieved by clock synchronization that guarantees bounded clock skew among all applications. Existing solutions for distributed runtime verification under partial synchrony against temporal logic specifications are exact but suffer from significant computational overhead. In this paper, we propose an approximate distributed monitoring algorithm for Signal Temporal Logic (STL) that mitigates this issue by abstracting away potential interleaving behaviors. This conservative abstraction enables a significant speedup of the distributed monitors, albeit with a tradeoff in accuracy. We address this tradeoff with a methodology that combines our approximate monitor with its exact counterpart, resulting in enhanced efficiency without sacrificing precision. We evaluate our approach with multiple experiments, showcasing its efficacy in both real-world applications and synthetic examples.},
  author       = {Bonakdarpour, Borzoo and Momtaz, Anik and Nickovic, Dejan and Sarac, Naci E},
  booktitle    = {24th International Conference on Runtime Verification},
  isbn         = {9783031742330},
  issn         = {1611-3349},
  location     = {Istanbul, Turkey},
  pages        = {282--301},
  publisher    = {Springer Nature},
  title        = {{Approximate distributed monitoring under partial synchrony: Balancing speed & accuracy}},
  doi          = {10.1007/978-3-031-74234-7_18},
  volume       = {15191},
  year         = {2024},
}

@inproceedings{18068,
  abstract     = {We study the following refinement relation between nondeterministic state-transition models: model ℬ strategically dominates model 𝒜 iff every deterministic refinement of 𝒜 is language contained in some deterministic refinement of ℬ. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as "strategy inclusion" between 𝒜 and ℬ: every strategy that resolves the nondeterminism of 𝒜 is dominated by a strategy that resolves the nondeterminism of ℬ. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata.},
  author       = {Henzinger, Thomas A and Mazzocchi, Nicolas Adrien and Sarac, Naci E},
  booktitle    = {35th International Conference on Concurrency Theory},
  isbn         = {9783959773393},
  issn         = {1868-8969},
  location     = {Calgary, Canada},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Strategic dominance: A new preorder for nondeterministic processes}},
  doi          = {10.4230/LIPIcs.CONCUR.2024.29},
  volume       = {311},
  year         = {2024},
}

@inproceedings{18175,
  abstract     = {Large-scale software repositories are a source of insights for software engineering. They offer an unmatched window into the software development process at scale. Their sheer number and size holds the promise of broadly applicable results. At the same time, that very size presents practical challenges for scaling tools and algorithms to millions of projects. A reasonable approach is to limit studies to representative samples of the population of interest. Broadly applicable conclusions can then be obtained by generalizing to the entire population. The contribution of this paper is a standardized experimental design methodology for choosing the inputs of studies working with large-scale repositories. We advocate for a methodology that clearly lays out what the population of interest is, how to sample it, and that fosters reproducibility. Along the way, we discourage researchers from using extrinsic attributes of projects such as stars, that measure some unclear notion of popularity.},
  author       = {Maj, Petr and Muroya Lei, Stefanie and Siek, Konrad and Di Grazia, Luca and Vitek, Jan},
  booktitle    = {38th European Conference on Object-Oriented Programming},
  isbn         = {9783959773416},
  issn         = {1868-8969},
  location     = {Vienna, Austria},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{The fault in our stars: Designing reproducible large-scale code analysis experiments}},
  doi          = {10.4230/LIPIcs.ECOOP.2024.27},
  volume       = {313},
  year         = {2024},
}

@article{18530,
  abstract     = {We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and HD specifications allow for game-based verification without an expensive determinization step. We show that the class of timed ω
-languages recognized by HD timed automata strictly extends that of deterministic ones, and is strictly included in those recognised by fully non-deterministic TA. For non-deterministic timed automata it is known that universality is already undecidable for safety/reachability TA. For history-deterministic TA with arbitrary parity acceptance, we show that timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete. For the subclass of TA with safety or reachability acceptance, one can decide (in EXPTIME) whether such an automaton is history-deterministic. If so, it can effectively determinized without introducing new automaton states.},
  author       = {Bose, Sougata and Henzinger, Thomas A and Lehtinen, Karoliina and Schewe, Sven and Totzke, Patrick},
  issn         = {1860-5974},
  journal      = {Logical Methods in Computer Science},
  number       = {4},
  pages        = {1--28},
  publisher    = {EPI Sciences},
  title        = {{History-deterministic timed automata}},
  doi          = {10.46298/lmcs-20(4:1)2024},
  volume       = {20},
  year         = {2024},
}

@inproceedings{18955,
  abstract     = {We give a simple proof that assuming the Exponential Time Hypothesis (ETH), determining the winner of a Rabin game cannot be done in time 2o(k log k) · nO(1), where k is the number of pairs of vertex subsets involved in the winning condition and n is the vertex count of the game graph. While this result follows from the lower bounds provided by Calude et al [SIAM J. Comp. 2022], our reduction is considerably simpler and arguably provides more insight into the complexity of the problem. In fact, the analogous lower bounds discussed by Calude et al, for solving Muller games and multidimensional parity games, follow as simple corollaries of our approach. Our reduction also highlights the usefulness of a certain pivot problem — Permutation SAT — which may be of independent interest.},
  author       = {Casares, Antonio and Pilipczuk, Marcin and Pilipczuk, Michał and Souza, Uéverton S. and Thejaswini, K. S.},
  booktitle    = {2024 Symposium on Simplicity in Algorithms},
  isbn         = {9781611977936},
  location     = {Alexandria, VA, United States},
  pages        = {160--167},
  publisher    = {Society for Industrial and Applied Mathematics},
  title        = {{Simple and tight complexity lower bounds for solving Rabin games}},
  doi          = {10.1137/1.9781611977936.16},
  year         = {2024},
}

@inproceedings{18599,
  abstract     = {Hypernode logic can reason about the prefix relation on stutter-reduced finite traces through the stutter-reduced prefix predicate. We increase the expressiveness of hypernode logic in two ways. First, we split the stutter-reduced prefix predicate into an explicit stutter-reduction operator and the classical prefix predicate on words. This change gives hypernode logic the ability to combine synchronous and asynchronous reasoning by explicitly stating which parts of traces can stutter. Second, we allow the use of regular expressions in formulas to reason about the structure of traces. This change enables hypernode logic to describe a mixture of trace properties and hyperproperties.

We show how to translate extended hypernode logic formulas into multi-track automata, which are automata that read multiple input words. Then we describe a fully online monitoring algorithm for monitoring k-safety hyperproperties specified in the logic. We have implemented the monitoring algorithm, and evaluated it on monitoring synchronous and asynchronous versions of observational determinism, and on checking the privacy preservation by compiler optimizations.},
  author       = {Chalupa, Marek and Henzinger, Thomas A and Oliveira da Costa, Ana},
  booktitle    = {Integrated Formal Methods},
  isbn         = {9783031765537},
  issn         = {1611-3349},
  pages        = {151--171},
  publisher    = {Springer Nature},
  title        = {{Monitoring extended hypernode logic}},
  doi          = {10.1007/978-3-031-76554-4_9},
  volume       = {15234},
  year         = {2024},
}

@inproceedings{18177,
  abstract     = {Partially Specified Boolean Networks (PSBNs) represent a family of Boolean models resulting from possible interpretations of unknown update logics. Hybrid extension of CTL (HCTL) has the power to express complex dynamical phenomena, such as oscillations or stability. We present BNClassifier to classify Boolean Networks corresponding to a given PSBN according to criteria specified in HCTL. The implementation of the tool is fully symbolic (based on BDDs). The results are visualised using the machine-learning-based technology of decision trees.},
  author       = {Beneš, Nikola and Brim, Luboš and Huvar, Ondřej and Pastva, Samuel and Šafránek, David},
  booktitle    = {Computational Methods in Systems Biology},
  isbn         = {9783031716706},
  issn         = {1611-3349},
  pages        = {19--26},
  publisher    = {Springer Nature},
  title        = {{BNClassifier: Classifying boolean models by dynamic properties}},
  doi          = {10.1007/978-3-031-71671-3_2},
  volume       = {14971},
  year         = {2024},
}

@inbook{18563,
  abstract     = {I give a personal account about the wave of new research activities that rose in the 1990s on the specification, verification, and control of real-time systems.},
  author       = {Henzinger, Thomas A},
  booktitle    = {Real Time and Such},
  editor       = {Graf, Susanne and Pettersson, Paul and Steffen, Bernhard},
  isbn         = {9783031737503},
  issn         = {1611-3349},
  pages        = {154--164},
  publisher    = {Springer Nature},
  title        = {{Reminiscences of a Real-Time Researcher}},
  doi          = {10.1007/978-3-031-73751-0_12},
  volume       = {15230},
  year         = {2024},
}

@inproceedings{15168,
  abstract     = {A linearly ordered (LO) k-colouring of a hypergraph is a colouring of its vertices with colours 1, … , k such that each edge contains a unique maximal colour. Deciding whether an input hypergraph admits LO k-colouring with a fixed number of colours is NP-complete (and in the special case of graphs, LO colouring coincides with the usual graph colouring). Here, we investigate the complexity of approximating the "linearly ordered chromatic number" of a hypergraph. We prove that the following promise problem is NP-complete: Given a 3-uniform hypergraph, distinguish between the case that it is LO 3-colourable, and the case that it is not even LO 4-colourable. We prove this result by a combination of algebraic, topological, and combinatorial methods, building on and extending a topological approach for studying approximate graph colouring introduced by Krokhin, Opršal, Wrochna, and Živný (2023).},
  author       = {Filakovský, Marek and Nakajima, Tamio Vesa and Opršal, Jakub and Tasinato, Gianluca and Wagner, Uli},
  booktitle    = {41st International Symposium on Theoretical Aspects of Computer Science},
  isbn         = {9783959773119},
  issn         = {1868-8969},
  location     = {Clermont-Ferrand, France},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title        = {{Hardness of linearly ordered 4-colouring of 3-colourable 3-uniform hypergraphs}},
  doi          = {10.4230/LIPIcs.STACS.2024.34},
  volume       = {289},
  year         = {2024},
}