In the untimed setting, it is well-known that the modal mu-calculus is more expressive than other modal logics such as LTL, CTL and CTL*. It can thus be considered a foundational logic for model-checking. In the timed setting, the status of similarly foundational logics is less satisfactory. There are timed extensions of modal logics, such as TCTL. Yet, the state of the art of timed mu-calculi is underdeveloped.

In this talk, I present a timed model mu-calculus $L_{rel}^{\mu,\nu}$ for encoding properties of systems modeled as timed automata. Our logic includes arbitrary fixpoints and an until-like modal operator for time elapses, and is shown to be strictly more expressive than existing timed modal mu-calculi introduced in the literature. It also enjoys decidable model checking, as it respects the traditional region-graph construction for timed automata. Additionally, I establish that, in contrast to other timed mu-calculi, $L_{rel}^{\mu,\nu}$ is strictly more expressive than Timed Computation Tree Logic (TCTL) in the setting of general timed automata, meaning that model checkers for $L_{rel}^{\mu,\nu}$ are immediately usable as model checkers for TCTL for general timed automata.

This is joint work with Rance Cleaveland and Peter Fontana, and appeared as [1].

[1] Cleaveland, R., Keiren, J.J.A., Fontana, P.: An Expressive Timed Modal Mu-Calculus for Timed Automata. In: Hillston, J. et al. (eds.) Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems., pp. 160–178. Springer Nature Switzerland, Cham (2024).

Regular word grammars are context-free grammars having restricted rules, that define all recognizable languages of words. This paper generalizes regular grammars from words to certain classes of graphs, by defining regular grammars for unordered unranked trees and graphs of tree-width 2 at most. The qualifier ``regular'' is justified because these grammars define precisely the recognizable (equivalently, CMSO-definable) sets of the respective graph classes. The proof of equivalence between regular and recognizable sets of graphs relies on the effective construction of a recognizer algebra of size doubly-exponential in the size of the grammar. This sets a 2EXPTIME upper bound on the (EXPTIME-hard) problem of inclusion of a context-free language in a regular language, for graphs of tree-width 2 at most. A further syntactic restriction of regular grammars suffices to capture precisely the MSO-definable sets of graphs of tree-width 2 at most, i.e., the sets defined by CMSO formulae without cardinality constraints. Moreover, we show that MSO-definability coincides with recognizability by algebras having an aperiodic parallel composition semigroup, for each class of graphs defined by a bound on the tree-width.

Although a database backing store is conceptually just a shared memory, modern stores have high internal complexity, for performance and fault tolerance reasons, and to support rich data types supporting incremental and/or convergent updates. As such complexity is bug-prone, this research proposes a correct-by-design approach, based on a set of formal specifications.

Possible executions are abstracted as a trace, a partial order of transactional events. Its valuation specifies the expected value of a key at each event, according to datatype semantics.

We specify two common variants of store, the eager, random-access map and the lazy, sequential-access journal. We show that both conform to the valuation, meaning that they are (i) safe, (ii) functionally equivalent, and (iii) causally consistent.

Finally, we propose a transaction semantics that is representative of common implementations and avoids the timestamp inversion anomaly. We show an equivalence between the trace and the transaction semantics; implying that maps and journals remain safe. Our results extend naturally to systems with stronger guarantees, such as classical assignment-based data types or strong consistency.

Finding Lyapunov functions to certify the stability of control systems has been an important topic for certifying safety-critical systems. Most existing methods on finding Lyapunov functions require access to the dynamics of the system. Accurately describing the complete dynamics of a control system however remains highly challenging in practice. Latest trend of using learning-enabled control systems further reduces transparency. Hence, a method for black-box systems would have much wider applications. In this talk, I will present our study on synthesizing Lyapunov functions for black-box systems. Our work stems from the idea of sampling and exploiting Lipschitz continuity to approximate the unknown dynamics. Given Lipschitz constants, one can derive a *non-statistical upper bounds* on approximation errors; hence a strong certification on this approximation can certify the unknown dynamics. We significantly improve this idea by directly approximating the Lie derivative of Lyapunov functions instead of the dynamics. We propose a framework based on the learner–verifier architecture from Counterexample-Guided Inductive Synthesis (CEGIS). Our insight of combining regional verification conditions and counterexample-guided sampling enables a guided search for samples to prove stability region-by-region. Our CEGIS algorithm further ensures termination. Our numerical experiments suggest that it is possible to prove the stability of 2D and 3D systems with a few thousands of samples. In comparison with the existing black-box approach using evenly-spaced sampling, our approach at the best case requires less than 0.01% of samples. The paper describing our latest results will be published in May at the conference on Hybrid Systems: Computation and Control 2025.

In recent years, many different methods for identifying hybrid automata from data have been proposed. However, most of these methods consider clean simulator data, and consequently do not perform well for noisy data measured from real systems. We address this shortcoming with a new approach for the identification of hybrid automata that is specifically designed to be robust to noise. In particular, we propose a new high-level strategy consisting of the following three steps: clustering based on the dynamics identified from a local dataset, state space partitioning using decision trees, and conversion of the decision tree to a hybrid automaton. In addition, we introduce several new concepts for the realization of the single steps. For example, we propose an automated regularization of the dynamic models used for clustering via rank adaption, as well as a new variant of the Gini impurity index for decision tree learning, tailored toward hybrid systems where different dynamics can be active within the same state space region. As our experiments on 19 challenging benchmarks with different characteristics demonstrate, in addition to being robust to both process and measurement noise, our approach avoids the need for extensive hyper-parameter tuning and also performs well for clean data without noise.

Verification of concurrent programs over infinite data domains is challenging: Algorithmic verifiers must infer inductive invariants that show correctness for all possible interleavings of program statements. Such invariants are often complex (requiring non-linear arithmetic, quantifiers, or reasoning with ghost variables) and out-of-reach for most invariant inference algorithms. In this talk, I present a series of works investigating how the notion of commutativity simplifies proofs of concurrent programs and thereby empowers algorithic verification. The idea of commutativity is based on the observation that some program statements can be reordered without affecting the outcome of an execution, and hence it suffices to verify a suitably-chosen subset of interleavings (rather than all interleavings) to conclude correctness of an entire concurrent program. We will see how commutativity-based combinatorial algorithms interact with symbolic reasoning over variables with infinite domains, and how commutativity can both extend the theoretical expressiveness and contribute to the practical success of verification approaches.

Together with Fixed Priority Scheduling, Earliest Deadline First (EDF) is the second leg on top of which a large portion of the research on real-time systems stands. At the heart of the EDF exact schedulability test, a pivotal role is played by the demand bound function test, which requires to evaluate whether the amount of work required to complete a set of jobs is less than or equal to the amount of time available. Such a test is checked over a set of time instants.

In this work, it is proposed a method that cuts drastically the set of constraints to be checked. Such a method is applicable also to tasks with release offset. Notably, it is proved that such a reduced set of constraints is minimal: it is not possible to reduce the set any further without losing the sufficiency of the test. The code to make this reduction is publicly available on GitHub.