Almost all problems in applied mathematics, including the analysis of dynamical systems, deal with spaces of real-valued functions on Euclidean domains in their formulation and solution. In this paper, we describe the the tool Ariadne, which provides a rigorous calculus for working with Euclidean functions. We first introduce the Ariadne framework, which is based on a clean separation of objects as providing exact, effective, validated and approximate information. We then discuss the function calculus as implemented in Ariadne, including polynomial function models which are the fundamental class for concrete computations. We then consider solution of some core problems of functional analysis, namely solution of algebraic equations and differential equations, and briefly discuss their use for the analysis of hybrid systems. We will give examples of C++ and Python code for performing the various calculations. Finally, we will discuss progress on extensions, including improvements to the function calculus and extensions to more complicated classes of system.

Neural networks find applications in many safety-critical systems that raise concerns about their deployment: Are we sure the network will never advise doing anything violating a set of safety constraints? Formal verification has been recently applied to prove whether an existing neural network is certified for some property (i.e., if it satisfies the property for all possible inputs) or not. Formal verification can prove that a network respects the property, but cannot fix a network that does not respect it. In this paper we focus on the automated synthesis of certified neural networks, that is, on how to automatically build a network that is guaranteed to respect some required properties. We exploit a Counter Example Guided Inductive Synthesis (CEGIS) loop that alternates Deep Learning, Formal Verification, and a novel data generation technique that augments the training data to synthesize certified networks in a fully automatic way. An application of a proof-of-concept implementation of the framework shows the feasibility of the approach.

Abstract There has been a growing interest in defining models of automata enriched with time, such as finite automata extended with clocks (timed automata). In this paper, we study deterministic timed finite state machines (TFSMs), i.e., finite state machines with a single clock, timed guards and timeouts which transduce timed input words into timed output words. We solve the problem of equivalence checking by defining a bisimulation from timed FSMs to untimed ones and vice versa. Moreover, we apply these bisimulation relations to build the intersection of two timed finite state machines by untiming them, intersecting them and transforming back to the timed intersection. It is known that many problems like inclusion and equivalence checking are undecidable for timed automata. Our results show that TFSMs correspond to a decidable subclass of timed automata that admits a restricted form of $$\varepsilon $$ ε -transitions (i.e., timeouts) where most of the relevant problems like equivalence and intersection are decidable.

Hybrid Systems are systems having a mixed discrete and continuous behaviour that cannot be characterized faithfully using either only discrete or only continuous models. A good framework for hybrid systems should support their compositional description and analysis, since commonly systems are specified by a composition of smaller subsystems, to cope with the complexity of their monolithic representation. Moreover, since the reachability problem for hybrid systems is undecidable, one should investigate the conditions that guarantee approximate computability of composition, when only approximations to the exact problem data are available.

Discovering association rules is a classical data mining task with a wide range of applications that include the medical, the financial, and the planning domains, among others. Modern rule extraction algorithms focus on static rules, typically expressed in the language of Horn propositional logic, as opposed to temporal ones, which have received less attention in the literature. Since in many application domains temporal information is stored in form of intervals, extracting interval-based temporal rules seems the natural choice. In this paper we extend the well-known algorithm APRIORI for rule extraction to discover interval temporal rules written in the Horn fragment of Halpern and Shoham's interval temporal logic.

In this paper, we consider the well-known modal logics $\mathbf{K}$, $\mathbf{T}$, $\mathbf{K4}$, and $\mathbf{S4}$, and we study some of their sub-propositional fragments, namely the classical Horn fragment, the Krom fragment, the so-called core fragment, defined as the intersection of the Horn and the Krom fragments, plus their sub-fragments obtained by limiting the use of boxes and diamonds in clauses. We focus, first, on the relative expressive power of such languages: we introduce a suitable measure of expressive power, and we obtain a complex hierarchy that encompasses all fragments of the considered logics. Then, after observing the low expressive power, in particular, of the Horn fragments without diamonds, we study the computational complexity of their satisfiability problem, proving that, in general, it becomes polynomial.

The use of robots in operating rooms improves safety and decreases patient recovery time and surgeon fatigue, but it introduces new potential hazards that can lead to severe injury or even the loss of human life. Thus, safety has been perceived as a crucial system property since the early days by the industry, the medical community, and the regulatory agents. In this article, we discuss the application of the mathematically rigorous technique known as Formal Verification to analyze the safety properties of a laser incision case study, and we assess its safe and predictable operation. Like all formal methods approaches, our analysis has three distinct components: a method to create a model of the system, a language to specify the properties, and a strategy to prove rigorously that the behavior of the model fulfills the desired properties. The model of the system takes the form of a hybrid automaton consisting of a discrete control part that operates in a continuous environment. The safety constraints are formalized as reachability properties of the hybrid automaton model, while the verification strategy exploits the capabilities of the tool A riadne to address the verification problem and answer the related questions ranging from safety to efficiency and effectiveness.

Clausal forms of logics are of great relevance in Artificial Intelligence, because they couple a high expressivity with a low complexity of reasoning problems. They have been studied for a wide range of classical, modal and temporal logics to obtain tractable fragments of intractable formalisms. In this paper we show that such restrictions can be exploited to lower the complexity of interval temporal logics as well. In particular, we show that for the Horn fragment of the interval logic AAbar (that is, the logic with the modal operators for Allen’s relations meets and met by) without diamonds the complexity lowers from NEXPTIME-complete to P-complete. We prove also that the tractability of the Horn fragments of interval temporal logics is lost as soon as other interval temporal operators are added to AAbar, in most of the cases.

We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of Horn formulas with diamonds is undecidable for any type of linear orders and semantics. On the contrary, satisfiability of Horn formulas with boxes is tractable over both discrete and dense orders under the reflexive semantics and over dense orders under the irreflexive semantics but becomes undecidable over discrete orders under the irreflexive semantics. Satisfiability of binary Horn formulas with both boxes and diamonds is always undecidable under the irreflexive semantics.

Modal logic is a paradigm for several useful and applicable formal systems in computer science, and, in particular, for temporal logics of various kinds. It generally retains the low complexity of classical propositional logic, but notable exceptions exist that present higher complexity or are even undecidable. In search of computationally well-behaved fragments, clausal forms and other sub-propositional restrictions of temporal and description logics have been recently studied. It is known that the Horn fragments of the modal logics between K and S4 are PSPACE-complete, keeping the same complexity of the the full propositional versions. In this paper, inspired by similar results in the temporal case, we sharpen the above result by showing that if we allow only box modalities in the language the Horn fragments of the modal logics between K and S4 become P-complete. Exploring the innermost reasons for the tractability of sub-Horn modal logics is a necessary condition to understand the behaviour of more expressive temporal and spatial languages under similar restrictions.

We introduce a platform-based design methodology that uses contracts to specify and abstract the components of a cyber-physical system (CPS), and provide formal support to the entire CPS design flow. The design is carried out as a sequence of refinement steps from a high-level specification to an implementation built out of a library of components at the lower level. We review formalisms and tools that can be used to specify, analyze, or synthesize the design at different levels of abstraction. For each level, we highlight how the contract operations can be concretely computed as well as the research challenges that should be faced to fully implement them. We illustrate our approach on the design of embedded controllers for aircraft electric power distribution systems.

In this paper we discuss the application of formal methods for the verification of properties of control systems designed for autonomous robotic systems. We illustrate our proposal in the context of surgery by considering the automatic execution of a simple action such as puncturing. To prove that a sequence of subtasks planned on pre-operative data can successfully accomplish the surgical operation despite model uncertainties, we specify the problem by using hybrid automata. We express the requirements of interest as questions about reachability properties of the hybrid automaton model. Then, we compare the different performance of current state-of-the art tools for reachability analysis of hybrid automata.

Description logics of the DL-Lite family are widely used in knowledge representation because of their low computational complexity and rather good expressivity sufficient to capture important conceptual modelling constructs and the OWL2 QL profile of the Ontology Web Language (OWL). Recently, various point-based temporal extensions of DL-Lite have been investigated. Here, we propose to extend DL-Lite with fragments of Halpern and Shoham's interval logic of Allen's relations (ℋ𝒮). We formally define such extensions and show how they can be successfully used in knowledge representation. In the quest for a decidable logic, we discuss the challanges in combining decidable fragments of ℋ𝒮 with DL-Lite.

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. Despite being relevant for a broad spectrum of application domains, ranging from temporal databases to artificial intelligence and verification of reactive systems, interval temporal logics still misses algorithms and tools capable of supporting them in an efficient way. In this paper, we approach the finite satisfiability problem for the simplest meaningful interval temporal logic (which is NEXPTIME-complete), namely A (also known as Right Propositional Neighborhood Logic), by means of a multi-objective combinatorial optimization model solved with three different multi-objective evolutionary algorithms. As a result we obtain a decision procedure that, although incomplete, turns out to be unexpectedly suitable and easy to implement with respect to classical complete algorithms. Moreover, this approach allows one to effectively search for the minimal model that satisfy a set of A-formulas without using any kind of normal form.

The relevance of formal verification methods is widely recognized in the computer science and embedded systems community. Recently, such methods have been introduced also within the control community, to help designers in developing control architectures for complex robotics systems. Robotic systems typically mix continuous and discrete behaviors that cannot be modeled faithfully using neither continuous-only nor discrete-only formalisms. The interaction of continuous and discrete dynamics makes the formal treatment of this kind of systems computationally very demanding, and justifies the need of studying new methods and algorithms. In this paper, we outline the current state-of-the-art, and describe some open problems in verification, refinement and implementation of autonomous robotic systems. We motivate the relevance of our analysis by means of an Autonomous Robotic Surgery test case.

In the last years hybrid automata have been applied in the design and verification of embedded systems. Once a hybrid model of the system has been proved to be correct with respect to the desired properties, it would be valuable to extract a correct-by-construction HW/SW implementation of it. This work discusses a methodology and a corresponding tool chain that allow to extract a HW/SW implementation of a controller modeled by a subclass of timed automata, named elastic controllers, operating in an environment represented by a hybrid automaton. The required tools have been either developed from scratch or extended from the current state-of-the-art in order to support an automated flow from hybrid automata specifications to correct-by-construction discrete implementations described in the SystemC language.

The introduction of Halpern and Shoham's modal logic of intervals (later on called HS) dates back to 1986. Despite its natural semantics, this logic is undecidable over all interesting classes of temporal structures. This discouraged research in this area until recently, when a number of non trivial decidable fragments have been found. This paper is a contribution toward the complete classification of HS fragments. Different combinations of Allen's interval relations begins (B), meets (A), and later (L), and their inverses A̅, B̅, and L̅, have been considered in the literature. We know from previous work that the combination ABB̅A̅ is decidable over finite linear orders and undecidable everywhere else. We extend these results by showing that ABB̅L̅ is decidable over the class of all (resp., dense, discrete) linear orders, and that it is maximal with respect to decidability over these classes: adding any other interval modality immediately leads to undecidability.

Unlike the Moon, the dark side of interval temporal logics is the one we usually see: their ubiquitous undesirability. Identifying minimal undecidable interval logics is thus a natural and important issue in the research agenda in the area. The decidability status of a logic often depends on the class of models (in our case, the class of interval structures)in which it is interpreted. In this paper, we have identified several new minimal undecidable logics amongst the fragments of Halpern-Shoham logic HS, including the logic of the overlaps relation, over the classes of all and finite linear orders, as well as the logic of the meet and subinterval relations, over the class of dense linear orders. Together with previous undecid ability results, this work contributes to delineate the border of the dark side of interval temporal logics quite sharply.

Decidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the last years. Even though most interval logics turnout to be undecidable, meaningful exceptions exist, such as the logics of temporal neighborhood and (some of) the logics of the subinterval relation. In this paper, we explore a different path to decidability: instead of restricting the set of modalities or imposing suitable semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema's CDT, and we suitably limit the nesting degree of modalities. The decidability of the satisfiability problem for the resulting CDT fragment is proved by embedding it into a well-known decidable prefix quantifier class of first-order logic, namely, the Bernays-Schonfinkel's class. In addition, we show that such a fragment is in fact NP-complete (theBernays-Schonfinkel's class is NEXPTIME-complete), and that any natural extension of it is undecidable.

Interval temporal logics formalize reasoning about interval structures over (usually) linearly ordered domains, where time intervals are the primitive ontological entities and truth of formulae is defined relative to time intervals, rather than time points. In this paper, we introduce and study Metric Propositional Neighborhood Logic (MPNL) over natural numbers. MPNL features two modalities referring, respectively, to an interval that is “met by” the current one and to an interval that “meets” the current one, plus an infinite set of length constraints, regarded as atomic propositions, to constrain the lengths of intervals. We argue that MPNL can be successfully used in different areas of artificial intelligence to combine qualitative and quantitative interval temporal reasoning, thus providing a viable alternative to well-established logical frameworks such as Duration Calculus. We show that MPNL is decidable in double exponential time and expressively complete with respect to a well-defined subfragment of the two-variable fragment FO2[N, =, <, s] of first-order logic for linear orders with successor function, interpreted over natural numbers. Moreover, we show that MPNL can be extended in a natural way to cover full FO2[N, =, <, s], but, unexpectedly, the latter (and hence the former) turns out to be undecidable.

Temporal reasoning plays an important role in artificial intelligence. Temporal logics provide a natural framework for its formalization and implementation. A standard way of enhancing the expressive power of temporal logics is to replace their unidimensional domain by a multidimensional one. In particular, such a dimensional increase can be exploited to obtain spatial counterparts of temporal logics. Unfortunately, it often involves a blow up in complexity, possibly losing decidability. In this paper, we propose a spatial generalization of the decidable metric interval temporal logic RPNL+INT, called Directional Area Calculus (DAC). DAC features two modalities, that respectively capture (possibly empty) rectangles to the north and to the east of the current one, and metric operators, to constrain the size of the current rectangle. We prove the decidability of the satisfiability problem for DAC, when interpreted over frames built on natural numbers, and we analyze its complexity. In addition, we consider a weakened version of DAC, called WDAC, which is expressive enough to capture meaningful qualitative and quantitative spatial properties and computationally better.

In this article, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two difficult cases: the relation of strict subintervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the current interval). For each of these logics, we establish a small pseudo-model property and construct a sound, complete and terminating tableau that searches systematically for existence of such a pseudo-model satisfying the input formulas. Both constructions are non-trivial, but the latter is substantially more complicated because of the presence of beginning and ending subintervals which require special treatment. We prove PSPACE completeness for both procedures and implement them in the generic tableau-based theorem prover Lotrec.

The effectiveness and the efficiency of functional ATPGs based on deterministic strategies is influenced by the computational model adopted to represent the design under test. In this context the extended finite state machine (EFSM) is a valuable model which reduces the risk of state explosion preserving relevant features of more traditional FSMs. This paper. defines a particular variant of EFSMs to manage properly both synchronous and asynchronous modules in a uniform way, and then it proposes theoretical basis to perform their composition by bounding state and transition growth. The aim of composition is to improve functional ATPG whose effectiveness and efficiency may be limited when separate EFSMs are used to model the design under test. Experimental results confirm this conjecture.

Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the 'right neighborhood' relation between intervals and explicit integer constraints for interval lengths. We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXP SPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.

We investigate fragments of Halpern-Shoham's interval logic HS involving the modal operators for the relations of left or right overlap of intervals. We prove that most of these fragments are undecidable, by employing a non-trivial reduction from the octant tiling problem.

Propositional interval temporal logics come into play in many areas of artificial intelligence and computer science. Unfortunately, most of them turned out to be (highly) undecidable. Some positive exceptions, belonging to the classes of neighborhood logics and of logics of subinterval relations, have been recently identified. In this paper, we address the decision problem for the future fragment of Propositional Neighborhood Logic (Right Propositional Neighborhood Logic) interpreted over trees and we positively solve it by providing a tableau-based decision procedure that works in exponential space. Moreover, we prove that the decision problem for the logic is EXPSPACE-hard, thus showing the optimality of the proposed procedure.