Home

The verification of asynchronous software components poses significant challenges due to the way components interleave and exchange input/output data concurrently. Compositional strategies aim to address this by separating the task of verifying individual components on local properties from the task of combining them to achieve global properties. This paper concentrates on employing symbolic model checking techniques to verify properties specified in Linear-time Temporal Logic (LTL) on asynchronous software components that interact through data ports. Unlike event-based composition, local properties can now impose constraints on input from other components, increasing the complexity of their composition. We consider both the standard semantics over infinite traces as well as the truncated semantics over finite traces to allow scheduling components only finitely many times. We propose a novel LTL rewriting approach, which converts a local property into a global one while considering the interleaving of infinite or finite execution traces of components. We prove the semantic equivalence of local properties and their rewritten version projected on the local symbols. The rewriting is also optimized to reduce formula size and to leave it unchanged when the temporal property is stutter invariant. These methods have been integrated into the OCRA tool, as part of the contract refinement verification suite. Finally, the different composition approaches were compared through an […]

---

Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian and co-Cartesian categories, where it governs guarded recursion and guarded iteration, respectively. Here, even more specifically, we deal with the semantics of call-by-value guarded iteration. It was shown by Levy, Power and Thielecke that call-by-value languages can be generally interpreted in Freyd categories, but in order to represent effectful function spaces, such a category must canonically arise from a strong monad. We generalize this fact by showing that representing guarded effectful function spaces calls for certain parameterized monads (in the sense of Uustalu). This provides a description of guardedness as an intrinsic categorical property of programs, complementing the existing description of guardedness as a predicate on a category.

---

Metric Temporal Logic (MTL) is a popular formalism to specify temporal patterns with timing constraints over the behavior of cyber-physical systems with application areas ranging in property-based testing, robotics, optimization, and learning. This paper focuses on the unified construction of sequential networks from MTL specifications over discrete and dense time behaviors to provide an efficient and scalable online monitoring framework. Our core technique, future temporal marking, utilizes interval-based symbolic representations of future discrete and dense timelines. Building upon this, we develop efficient update and output functions for sequential network nodes for timed temporal operations. Finally, we extensively test and compare our proposed technique with existing approaches and runtime verification tools. Results highlight the performance and scalability advantages of our monitoring approach and sequential networks.

---

We study two subclasses of the class of automatic structures: automatic structures of polynomial growth and Presburger structures. We present algebraic characterisations of the groups and the equivalence structures in these two classes.

---

Linear Logic refines Intuitionnistic Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which can describe the resource management or the complexity analysis of a program. From an other perspective, Differential Linear Logic is an extension which allows the linearization of proofs. In this article, we merge these two directions by first defining a differential version of Graded linear logic: this is made by indexing exponential connectives with a monoid of differential operators. We prove that it is equivalent to a graded version of previously defined extension of finitary differential linear logic. We give a denotational model of our logic, based on distribution theory and linear partial differential operators with constant coefficients.

---