Compositional Reasoning and Model Checking of Asynchronous Systems on Variations of LTL

Formal verification is a method that offers mathematically rigorous techniques for verifying system correctness. While it has become a foundational tool in the design and verification of critical systems, its application to modern, real-world systems is increasingly hindered by a combination of fundamental challenges: scalability, expressiveness and system complexity. Scalability issues arise from the explosion of the state space caused by concurrency, interleaving, and system size. Expressiveness is another key difficulty: specification languages must be able to capture arithmetic constraints, real-time specifications, and hyperproperties–i.e., properties relating multiple executions, such as security or diagnosability. Finally, system features such as non-deterministic scheduling, real-time constraints, or shared-memory further complicate modeling and aggravate the other two challenges. This thesis addresses these three problems as follows. First, in the context of Verification Modulo Theories, we propose an ad-hoc invariant based algorithm for verifying a class of LTL modulo theory properties by leveraging the notion of relative safety. This contributes to a more scalable verification strategy for non-trivial properties beyond traditional safety. We also present an open framework supporting both finite and infinite trace semantics. Second, we develop a compositional framework for asynchronous systems where components are specified in LTL modulo theory. The semantics naturally account for component termination or failure, improving modular reasoning. This approach is extended to real-time systems through Metric Temporal Logic with Skewed Clocks (MTLSK), enabling the verification of time-sensitive distributed behaviours. Third, we tackle hyperproperty verification via two distinct contributions: a k-induction-based method for verifying ∀∃ hyperproperties, and the introduction of an asynchronous temporal logic (GHyperLTLS+C). We identify a decidable, non-prenex fragment expressive enough for diagnosability, and design model checking procedures for the prenex fragment over finite traces. Together, these contributions advance symbolic verification by improving its scalability, expressiveness, and support for complex system models.