Word-representable graphs are - by Kitaev and Pyatkin - undirected graphs that can be encoded by a word: there is an edge between two nodes iff the corresponding letters alternate in the representing word. In this work, we present a novel extension of this notion to directed graphs and explore the properties of this generalisation. We prove that some directed graphs are not word-representable and investigate the directed graphs represented by uniform words. Moreover, we examine word-representability of several classes of directed graphs and show that every acyclic and every transitive directed graph is word-representable. Among other complexity results, we prove that deciding whether a directed graph is word-representable is NP-hard, while a maximum complete induced subgraph can be found in polynomial time for these graphs.
Reachability is a fundamental problem arising across many areas of mathematics, including dynamical systems, number theory, automata theory, group theory, geometry, topology, and algebra. Given an initial configuration and a collection of transformations, can a designated target be reached? This survey develops a common perspective on reachability, focusing on piecewise-affine maps, nondeterministic affine systems, low-dimensional matrix semigroups, matrix equations, and linear recurrence sequences. Throughout, we highlight structural features that govern decidability and computational complexity, identify connections between these models, and formulate mathematical challenges and open problems at the boundaries between these areas.
The study of hybrid systems presents significant challenges in verification problems as the set of possible trajectories might be infinite-dimensional. In this paper, we propose a parametric Statistical Model Checking (pSMC) technique applied to hybrid reaction-diffusion systems with non-linear dynamics. The proposed approach extends the pSMC framework of [2]. It provides guarantees of precision and confidence using a piecewise polynomial approximation of the probability of satisfying a property. In addition, as a proof of concept, this technique is applied to a case study where we show that, the same precision, and the computation cost is lower than an iterative Monte Carlo method.
In this paper, we study two variants of timed alternating simulation on multi-player turn-based hybrid games and investigate their relationship with two variants of Timed Alternating-time Temporal Logic (TATL) whose semantics are defined on hybrid games. The first simulation, defined for a particular coalition , preserves coalition strategies and the satisfaction of TATL formulae which use bounded until and release operators. The second relation requires the values of the (continuous) variables in I to be preserved both before and after resets. We relate it to a new version of TATL, called Real-Valued ATL (RVATL), which extends TATL with predicates over the current values of the variables in I and their values immediately before resets. We then show that this latter simulation preserves the satisfaction of I- restricted RVATL formulae. We also investigate the algorithmic complexity of the induced simulation problems. We show that it is undecidable in general, already for single-player stopwatch games, but EXPTIME-complete for initialized singular turn-based games.
We discuss some recent approaches to game-theoretic semantics (GTS), a useful alternative to the traditional Tarski-style compositional semantics of logic. One attractive feature of GTS is that model-checking upper bounds for logical systems can often be obtained directly by considering the corresponding alternating Turing machines. Our focus is on semantic games equipped with clocks, i.e., resources that control recursive behaviour during play and give rise to timed variants of reachability games. Such clock-based semantic frameworks naturally suggest variants of logical systems with different computational properties. We review some developments related to these themes, focusing on systems derived from the modal μ -calculus while also discussing applications to temporal logic.
