Angluin's L$^*$ algorithm learns the minimal deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively correct (PAC) version substitutes an equivalence query by numerous random membership queries to get a high level confidence to the answer. Thus it can be applied to any kind of device and may be viewed as an algorithm for synthesizing an automaton abstracting the behavior of the device based on observations. Here we are interested on how Angluin's PAC learning algorithm behaves for devices which are obtained from a DFA by introducing some noise. More precisely we study whether Angluin's algorithm reduces the noise and produces a DFA closer to the original one than the noisy device. We propose several ways to introduce the noise: (1) the noisy device inverts the classification of words w.r.t. the DFA with a small probability, (2) the noisy device modifies with a small probability the letters of the word before asking its classification w.r.t. the DFA, (3) the noisy device combines the classification of a word w.r.t. the DFA and its classification w.r.t. a counter automaton, and (4) the noisy DFA is obtained by a random process from two DFA such that the language of the first one is included in the second one. Then when a word is accepted (resp. rejected) by the first (resp. second) one, it is also accepted (resp. rejected) and in the remaining cases, it is accepted with probability 0.5. Our main experimental contributions consist in showing that: (1) Angluin's algorithm behaves well whenever the noisy device is produced by a random process, (2) but poorly with a structured noise, and, that (3) is able to eliminate pathological behaviours specified in a regular way. Theoretically, we show that randomness almost surely yields systems with non-recursively enumerable languages.

Decisiveness of infinite Markov chains with respect to some (finite or infinite) target set of states is a key property that allows to compute the reachability probability of this set up to an arbitrary precision. Most of the existing works assume constant weights for defining the probability of a transition in the considered models. However numerous probabilistic modelings require the (dynamic) weight to also depend on the current state. So we introduce a dynamic probabilistic version of counter machine (pCM). After establishing that decisiveness is undecidable for pCMs even with constant weights, we study the decidability of decisiveness for subclasses of pCM. We show that, without restrictions on dynamic weights, decisiveness is undecidable with a single state and single counter pCM. On the contrary with polynomial weights, decisiveness becomes decidable for single counter pCMs under mild conditions. Then we show that decisiveness of probabilistic Petri nets (pPNs) with polynomial weights is undecidable even when the target set is upward-closed unlike the case of constant weights. Finally we prove that the standard subclass of pPNs with a regular language is decisive with respect to a finite set whatever the kind of weights.

Abstract This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning. This model may then be analyzed using model checking as a verification technique. The term property-directed reflects the idea that our procedure is guided and controlled by the given property rather than performing the two steps separately. We show that this not only allows us to discover small counterexamples fast, but also to generalize them by pumping toward faulty flows hinting at the underlying error in the RNN. We also show that our method can be efficiently used for adversarial robustness certification of RNNs.

Web services provide a general basis of convenient access and operation for cloud applications. However, such services become very vulnerable when being attacked, especially in the situation where service continuity is one of the most important requirements. This issue highlights the necessity to apply reliable and formal methods to attack tolerance in Web services. In this paper, we propose a Coloured Petri Nets based method for attack tolerance by modelling and analysing basic behaviours of attack-network interaction, attack detectors and their tolerance solutions. Furthermore, complex attacks can be analysed and tolerance solutions deployed by identifying these basic attack-network interactions and composing their solutions. The validity of our method is demonstrated through a case study on attack tolerance in cloud-based medical information storage.

A central task in partially observed controllable system is to detect or prevent the occurrence of certain events called faults. Systems for which one can design a controller avoiding the faults are called actively safe. Otherwise, one may require that a fault is eventually detected, which is the task of diagnosis. Systems for which one can design a controller detecting the faults are called actively diagnosable. An intermediate requirement is prediction, which consists in determining that a fault will occur whatever the future behaviour of the system. When a system is not predictable, one may be interested in designing a controller to make it so. Here we study the latter problem, called active prediction, and its associated property, active predictability. In other words, we investigate how to determine whether or not a system enjoys the active predictability property, i.e., there exists an active predictor for the system. Our contributions are threefold. From a semantical point of view, we refine the notion of predictability by adding two quantitative requirements: the minimal and maximal delay before the occurence of the fault, and we characterize the requirements fulfilled by a controller that performs predictions. Then we show that active predictability is EXPTIME-complete where the upper bound is obtained via a game-based approach. Finally we establish that active predictability is equivalent to active safety when the maximal delay is beyond a threshold depending on the size of the system, and we show that this threshold is accurate by exhibiting a family of systems fulfilling active predictability but not active safety.

In this paper, we propose an approach to ensure the diagnosability of a partially controllable system. Given a model of correct and faulty behaviors of a partially observable discrete event system, equipped with a set of elementary actions that do not intertwine with autonomous events, we search a diagnosability plan, i.e., a sequence of applicable actions that leads the system from an initial belief state (a set of potentially current states) to a diagnosable belief state, in which the system is then left to run freely. This helps in reducing the diagnosis interaction with running systems and can be applied, e.g., on the output of a repair plan, like in power networks. The two successive stages of this approach keep diagnosability planning, including diagnosability tests, in PSpace in comparison to the Exptime test for the more complex active diagnosability used usually in such cases. For this, we propose to construct incrementally the twin plant structure of the given system and to exploit its parts already constructed while testing the candidate plans and constructing its next parts. This helps in pruning the twin plant constructions and many non-diagnosability plan tests. We have created a special benchmark and tested three proposed methods, according to the recycling level of twin plants construction, with one cost function used for plan optimality and an optional heuristics.

Verifying behavioral or safety properties of hybrid systems, either at design stage such as state reachability and diagnosability, or on-line such as fault detection and isolation is a challenging task. We are concerned here with abstractions oriented towards hybrid systems diagnosability checking. The verification can be done on the abstraction by classical methods developed for discrete event systems extended with time constraints, which provide a counterexample in case of non-diagnosability. The absence of such a counterexample proves the diagnosability of the original hybrid system. In the presence of a counterexample, the first step is to check if it is not a spurious effect of the abstraction and actually exists for the hybrid system, witnessing thus non-diagnosability. Otherwise, we show how to refine the abstraction, guided by the elimination of the counterexample, and continue the process of looking for another counterexample until either a final result is obtained or we reach an inconclusive verdict. We make use of qualitative modeling and reasoning to compute discrete abstractions. Abstractions as timed automata are particularly studied as they allow one to handle time constraints that can be captured at a qualitative level from the hybrid system.

Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on the diagnosability property of a system. Diagnosability describes the system ability to determine whether a given fault has effectively occurred based on the observations. However, this is a very strong property that requires generally high number of sensors to be satisfied. Consequently, it is not rare that developing a diagnosable system is too expensive. To solve this problem, in this paper, we first define a new system property called manifestability that represents the weakest requirement on faults and observations for having a chance to identify on line fault occurrences and can be verified at design stage. Then, we propose an algorithm with PSPACE complexity to automatically verify it.

Choreographies are contracts specifying from a global point of view the legal interactions that must take place among a set of services. Such a contract may serve as a reference in the development of concurrent distributed system, whether it is achieved following a top-down or a bottom-up approach. In this article, we present VerChor, a generic, modular, and extensible framework for supporting the development based on choreographies. It relies on a choreography intermediate format (CIF) into which several existing choreography description languages can be transformed. VerChor builds around a set of formal properties whose verification is central to choreography-based development. To support this development process, we propose a connection between CIF and the CADP verification toolbox, which enables the full automation of the aforementioned properties. Finally, we illustrate a practical use of the VerChor framework through its integration with the Eclipse BPMN 2.0 designer.

Diagnosability is an important system property that determines at design stage how accurate any diagnostic reasoning can be on a partially observed system. A fault in a discrete-event system is diagnosable iff its occurrence can always be deduced from enough observations. It is well known that centralized diagnosability approaches lead to combinatorial explosion of the search space since they assume the existence of a monolithic model of the system. This is why very recently the distributed approaches for diagnosability began to be investigated, relying on local objects. On the other hand, diagnosis objectives are generalized from fault event to fault pattern that can represent multiple faults, repeating fault, sequences of significant events, repair of faults, etc. For pattern case, most existing approaches are centralized. In this paper, we propose a new distributed framework for pattern diagnosability. We first show how to recognize patterns by incrementally constructing local pattern recognizers through extended subsystems. Then we propose a structure called regional pattern verifier that is constructed from the subsystem where the pattern is completely recognized before showing how to abstract just the necessary and sufficient diagnosability information to further save the search space. Then the global consistency checking is based on another local structure called abstracted local twin checker to analyze pattern diagnosability. In this way, we avoid constructing global objects both for pattern recognition and for pattern diagnosability. The correctness of our distributed algorithm is theoretically proved and its efficiency experimentally demonstrated by the results of the implementation.

The paper proposes a decentralized diagnosis approach for a set of choreographed BPEL Web services, where a local diagnoser is associated to each BPEL service and cooperates with a coordinator. The local diagnosis is based on a Colored Petri Nets model enriched with I/O data dependency relations represented with color propagation functions (A preliminary version of centralized local diagnosis has been presented in). By applying the multiset marking calculation equation, a diagnosis inequations system is constructed and solved to retrieve a local diagnosis. The coordinator updates the global diagnosis until reaching a final consistency.

Diagnosability is a crucial property that determines at design stage how accurate any diagnosis algorithm can be on a partially observable system. Recent work on diagnosability has generalized fault event case to pattern case, which can describe more general objectives for diagnosis problem, but based on global model and global twin plant construction. In this paper, we propose an original framework to solve pattern diagnosability in a distributed way to avoid calculating global objects. We first show how to incrementally accomplish pattern recognition without building global model by propagating only diagnosability relative information between components. Then an efficient way to construct pattern verifier is proposed, which is inspired from the classical twin plant method but with smaller state space, to search for partial critical paths, whose global consistency is subsequently checked. Meanwhile we prove that the result obtained from our distributed approach is on an equality with that from the centralized one but the evaluation result shows that our search state space exploited is only a small subpart of the global twin plant, whose construction is unavoidable in the centralized approach.