Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.

We define HyPOL, a local hyper logic for partial order models, expressing properties of sets of runs. These properties depict shapes of causal dependencies in sets of partially ordered executions, with similarity relations defined as isomorphisms of past observations. Unsurprisingly, since comparison of projections are included, satisfiability of this logic is undecidable. We then address model checking of HyPOL and show that, already for safe Petri nets, the problem is undecidable. Fortunately, sensible restrictions of observations and nets allow us to bring back model checking of HyPOL to a decidable problem, namely model checking of MSO on graphs of bounded treewidth.

Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe convergent Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.

We consider opacity questions where an observation function provides to an external attacker a view of the states along executions and secret executions are those visiting some state from a fixed subset. Disclosure occurs when the observer can deduce from a finite observation that the execution is secret, the epsilon-disclosure variant corresponding to the execution being secret with probability greater than 1 - epsilon. In a probabilistic and non deterministic setting, where an internal agent can choose between actions, there are two points of view, depending on the status of this agent: the successive choices can either help the attacker trying to disclose the secret, if the system has been corrupted, or they can prevent disclosure as much as possible if these choices are part of the system design. In the former situation, corresponding to a worst case, the disclosure value is the supremum over the strategies of the probability to disclose the secret (maximisation), whereas in the latter case, the disclosure is the infimum (minimisation). We address quantitative problems (comparing the optimal value with a threshold) and qualitative ones (when the threshold is zero or one) related to both forms of disclosure for a fixed or finite horizon. For all problems, we characterise their decidability status and their complexity. We discover a surprising asymmetry: on the one hand optimal strategies may be chosen among deterministic ones in maximisation problems, while it is not the case for minimisation. On the other hand, for the questions addressed here, more minimisation problems than maximisation ones are decidable.

Non-interference (NI) is a property of systems stating that confidential actions should not cause effects observable by unauthorized users. Several variants of NI have been studied for many types of models but rarely for true concurrency or unbounded models. This work investigates NI for High-level Message Sequence Charts (HMSCs), a scenario language for the description of distributed systems, based on composition of partial orders. We first propose a general definition of security properties in terms of equivalence among observations of behaviors. Observations are naturally captured by partial order automata, a formalism that generalizes HMSCs and permits assembling partial orders. We show that equivalence or inclusion properties for HMSCs (and hence for partial order automata) are undecidable, which means in particular that NI is undecidable for HMSCs. We hence consider decidable subclasses of partial order automata and HMSCs. Finally, we define weaker local properties, describing situations where a system is attacked by a single agent, and show that local NI is decidable. We then refine local NI to a finer notion of causal NI that emphasizes causal dependencies between confidential actions and observations and extend it to causal NI with (selective) declassification of confidential events. Checking whether a system satisfies local and causal NI and their declassified variants are PSPACE-complete problems.

Interrupt Timed Automata (ITA) are an expressive timed model, introduced to take into account interruptions according to levels. Due to this feature, this formalism is incomparable with Timed Automata. However several decidability results related to reachability and model checking have been obtaine d. We add auxiliary clocks to ITA, thereby extending its expressive power while preserving decidability of reachability. Moreover, we define a parametrized version of ITA, with polynomials of parameters appearing in guards and updates. While parametric reasoning is particularly relevant for timed models, it very often leads to undecidability results. We prove that various reachability problems, including robust reachability, are decidable for this model, and we give complexity upper bounds for a fixed or variable number of clocks, levels and parameters.

Opacity is a general language-theoretic framework in which several security properties of a system can be expressed. Its parameters are a predicate, given as a subset of runs of the system, and an observation function, from the set of runs into a set of observables. The predicate describes secret information in the system and, in the possibilistic setting, it is opaque if its membership cannot be inferred from observation. In this paper, we propose several notions of quantitative opacity for probabilistic systems, where the predicate and the observation function are seen as random variables. Our aim is to measure (i) the probability of opacity leakage relative to these random variables and (ii) the level of uncertainty about membership of the predicate inferred from observation. We show how these measures extend possibilistic opacity, we give algorithms to compute them for regular secrets and observations, and we apply these computations on several classical examples. We finally partially investigate the non-deterministic setting.

Controller synthesis consists in automatically generating a controller to restrict a hardware or software system so that it respects given requirements, for instance safety properties. Existing synthesis tools for discrete event systems mainly solve the problem for systems described in low-level formalisms.

Interrupt Timed Automata (ITA) have been introduced to model multi-task systems with interruptions. They form a subclass of stopwatch automata, where the real valued variables (with rate 0 or 1) are organized along priority levels. While reachability is undecidable with usual stopwatches, the problem was proved decidable for ITA. In this work, after giving answers to some questions left open about expressiveness, closure, and complexity for ITA, our main purpose is to investigate the verification of real time properties over ITA. While we prove that model checking a variant of the timed logic TCTL is undecidable, we nevertheless give model checking procedures for two relevant fragments of this logic: one where formulas contain only model clocks and another one where formulas have a single external clock.

System and program verification has been a large area of research since the introduction of computers in industrial systems. It is an especially important issue for critical systems, where errors can cause human and financial damages. Programmable Logic Controllers (PLCs) are now widely used in many industrial systems and verification of the corresponding programs has already been studied in various contexts for a few years, for the benefit of users and system designers. First restricted to an untimed setting, verification was recently extended to systems where quantitative constraints are needed, possibly related to time elapsing. For instance, timed features like TON (Timers ON delay), used in PLC programs, were modeled with timed automata, thus increasing the size of the verification problems addressed.

Timed automata are among the most widely studied models for real-time systems. Silent transitions, i.e., ϵ-transitions, have already been proposed in the original paper on timed automata by Alur and Dill [3]. We show that the class TL ϵ of timed languages recognized by automata with ϵ-transitions, is more robust and more expressive than the corresponding class TL without ϵ-transitions. We then focus on ϵ-transitions without reset, i.e. ϵ-transitions which do not reset clocks. We propose an algorithm to construct, given a timed automaton, an equivalent one without such transitions. This algorithm is in two steps, it first suppresses the cycles of ϵ-transitions without reset and then the remaining ones. Then, we prove that a timed automaton such that no ϵ-transition which resets clocks lies on any directed cycle, can be effectively transformed into a timed automaton without ϵtransitions. Interestingly, this main result holds under the assumption of non-Zenoness and it is false otherwise. To complete the picture, we exhibit a simple timed automaton with an ϵ-transition, which resets some clock, on a cycle and which is not equivalent to any ϵ-free timed automaton. To show this, we develop a promising new technique based on the notion of precise action. This paper presents a synthesis of the two conference communications [9] and [13].