Search

In this paper we address partial information games restricted to memoryless strategies.Our contribution is threefold. First, we prove that for partial information games, deciding the existence of memoryless strategies is NP-complete, even for games with only reachability objectives. %This result is interesting in itself since in the case of games with total information it is already proven that memory is not necessary to win the game. The second contribution of this paper is a SAT/SMT-based encoding of a partial information game altogether with the correctness proof of this encoding. Finally, we apply our methodology to automatically synthesize strategies for oblivious mobile robots. We first prove that synthesizing memoryless strategies is equivalent to providing a distributed protocol for the robots. Then, we use an SMT-solver to synthesize strategies for the gathering problem in a particular configuration ($SP_4$), open case in distributed computing theory for more than a decade. Interestingly, our work is the first that combines two-player games theory and SMT-solvers in the context of mobile robots with promising results and therefore it is highly valuable for distributed computing theory where a broad class of open problems are still to be investigated.

International audience; We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a Strongly Connected Component (SCC) enumeration, support generalized Büchi acceptance, and require no synchronization points nor recomputing procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks. The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used.

International audience; We study the reactive synthesis problem (RS) for specifications given in Metric Interval Temporal Logic (MITL). RS is known to be undecidable in a very general setting, but on infinite words only; and only the very restrictive BResRS subcase is known to be decidable (see D'Souza et al. and Bouyer et al.). In this paper, we precise the decidabil-ity border of MITL synthesis. We show RS is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit BResRS and introduce an efficient on-the-fly algorithm to solve it.

International audience; Modelling and simulation have been heavily used in epidemiology, for instance to study the transmission of infectious diseases, their pathogenicity and their propagation. A major hindrance to modelling in epidemiology is the mixing of concerns that ought to be separated. The most obvious one is the computer implementation that should not be mixed with domain aspects. But several domain concerns should also be separated from the core epidemiological ones. These include the distribution of the studied populations into spatial regions, age intervals, sexes, species, viral strains... We propose an approach that relies on a mathematical model of the dynamics of a compartment-based population. The separation of domain concerns is provided by expressing each one as a stochastic automaton and combining them with a tensor sum. A DSL, Kendrick, and a tool, support this approach that has been validated on several case studies.

International audience; Due to contextual traffic conditions, the computation of optimized or shortest paths is a very complex problem for both drivers and autonomous vehicles. This paper introduces a reinforcement learning mechanism that is able to efficiently evaluate path durations based on an abstraction of the available traffic information. The authors demonstrate that a cache data structure allows a permanent access to the results whereas a lazy politics taking new data into account is used to increase the viability of those results. As a client of the proposed learning system, the authors consider a contextual path planning application and they show in addition the benefit of integrating a client cache at this level. Our measures highlight the performance of each mechanism, according to different learning and caching strategies.

International audience; Mathematical modelling of infectious diseases often uses simulation models in order to explore transmission mechanisms and to plan potential management strategies to control the epidemics. However, bridging the gap between the conceptual model of epidemiology and its simulation on computer can lead to some issues related to the lack of expressiveness of implemented models and their reusability and adaptability to new circumstances due to detail computer instructions in General-purpose Programming Languages (GPLs). In this paper, we propose to develop a Domain Specific Language (DSL) for expressively specifying mathematical models of epidemiology and to construct a flexible simulation environment for investigating them. We then use our proposed approach to experiment the measles model in different epidemiological aspects. Our platform is also validated through statistical comparisons between time series generated and theoretical expectations, consequently keeping the link with literature on mathematical epidemiology.

International audience; A well-known framework with strong potential for epidemic prediction and the ability to incorporate realistic contact structures is edge-based compartmental modeling (EBCM). However, models built from this framework lead to a multiplication of ordinary differential equations and many parameters to be estimated, which make the models complex and difficult to extend or to reuse. The Kendrick approach has shown promising results in generalizing compartmental models to take into account aspects of contact networks while preserving the separation of concerns, thus allowing to define modular, extensible and reusable models. But this generalization of compartmental models to contact network aspects is still limited to a few contact networks. In this paper, we present an attempt to extend Kendrick's approach from an approximation of EBCM models to further support aspects of contact networks, thereby improving the predictive quality of models with significant heterogeneity in contact structure, while maintaining the simplicity of compartmental models. This extension consists of an integration of the basic reproductive number R 0 into the compartmental SIR framework. This attempted is validated using Miller's mass action and the approximation of EBCM configuration model.

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. Here, we study the extension of the classical framework onto infinite inputs: We introduce reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and study expressiveness, closure properties, and the complexity of verification problems. We show that almost all classes of automata have pairwise incomparable expressiveness, both in the deterministic and the nondeterministic case; a result that sharply contrasts with the well-known hierarchy in the ω-regular setting. Furthermore, emptiness is shown decidable for Parikh automata with reachability or Büchi acceptance, but undecidable for safety and co-Büchi acceptance. Most importantly, we show decidability of model checking with specifications given by deterministic Parikh automata with safety or co-Büchi acceptance, but also undecidability for all other types of automata. Finally, solving games is undecidable for all types., LIPIcs, Vol. 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022), pages 40:1-40:20

International audience; The reverse engineering of behavioral models consists in extracting high-level models that help understand the behavior of existing software systems. In the context of reverse engineering of sequence diagrams, most approaches strongly depend on the static analysis and instrumentation of the source code to produce correct diagrams that take into account control flow structures such as alternative blocks ("if"s) and repeated blocks ("loop"s). This approach is not possible with systems for which no source code is available anymore (e.g. some legacy systems). In this paper, we propose an approach for the reverse engineering of sequence diagrams from the analysis of execution traces produced dynamically by an object-oriented application. Our approach is fully based on dynamic analysis and reuses the k-tail merging algorithm to produce a Labeled Transition System (LTS) that merges the collected traces. This LTS is then translated into a sequence diagram which contains alternatives and loops. A prototype of this approach has been tested with a real world application that has been developed independently from the present work. Our results show that this approach can produce sequence diagrams in reasonable time and suggest that these diagrams are helpful in understanding the behavior of the underlying application.

International audience

International audience; Digital twin technology establishes the future development vision for Industry 4.0, and is also an important exploration direction for the Model-Driven Engineering (MDE) paradigm. Because it builds a more flexible and communicative production system through models that spans life cycle, hierarchy and architecture. The standard proposed under the concept of Industry 4.0, the Asset Administration Shell (AAS), provides a syntactic interoperability interface for all assets involved in smart factories. However, there is still a need to fill the gap regarding semantic interoperability, in order to allow efficient interactions between Industry 4.0 components. Ontologies are a good candidate because they provide formal semantics expressed using a knowledge representation language, and in addition, there are many associated mature tools for reasoning and inference. Therefore, we propose a modeling approach that provides semantic interoperability for AAS-based digital twins using ontologies.

International audience; An automaton is history-deterministic (HD) if one can safely resolve its non-deterministic choices on the fly. In a recent paper, Henzinger, Lehtinen and Totzke studied this in the context of Timed Automata [9], where it was conjectured that the class of timed ω-languages recognised by HD-timed automata strictly extends that of deterministic ones. We provide a proof for this fact.

Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run. Thereby, they preserve many of the desirable properties of finite automata. Deterministic Parikh automata are strictly weaker than nondeterministic ones, but enjoy better closure and algorithmic properties. This state of affairs motivates the study of intermediate forms of nondeterminism. Here, we investigate history-deterministic Parikh automata, i.e., automata whose nondeterminism can be resolved on the fly. This restricted form of nondeterminism is well-suited for applications which classically call for determinism, e.g., solving games and composition. We show that history-deterministic Parikh automata are strictly more expressive than deterministic ones, incomparable to unambiguous ones, and enjoy almost all of the closure and some of the algorithmic properties of deterministic automata., arXiv admin note: text overlap with arXiv:2207.07694

International audience

International audience

International audience; Defenders fighting against Advanced Persistent Threats need to discover the propagation area of an adversary as quickly as possible. This discovery takes place through a phase of an incident response operation called Threat Hunting, where defenders track down attackers within the compromised network. In this article, we propose a formal model that dissects and abstracts elements of an attack, from both attacker and defender perspectives. This model leads to the construction of two persistent graphs on a common set of objects and components allowing for (1) an omniscient actor to compare, for both defender and attacker, the gap in knowledge and perceptions; (2) the attacker to become aware of the traces left on the targeted network; (3) the defender to improve the quality of Threat Hunting by identifying false-positives and adapting logging policy to be oriented for investigations. In this article, we challenge this model using an attack campaign mimicking APT29, a real-world threat, in a scenario designed by the MITRE Corporation. We measure the quality of the defensive architecture experimentally and then determine the most effective strategy to exploit data collected by the defender in order to extract actionable Cyber Threat Intelligence, and finally unveil the attacker.

International audience; Priced timed games are two-player zero-sum games played on priced timed au-tomata (whose locations and transitions are labeled by weights modeling the price of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the price to reach a target location, respectively. We consider priced timed games with one clock and arbitrary integer weights and show that, for an important subclass of theirs (the so-called simple priced timed games), one can compute, in exponential time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called negative-reset-acyclic priced timed games (with arbitrary integer weights and one clock). The decidability status of the full class of priced timed games with one-clock and arbitrary integer weights still remains open.

International audience; finElink is a recommendation system that provides guidance to French innovative companies with regard to their financing strategy through public funding mechanisms. Analysis of financial data from former funding recipients partially feeds the recommendation system. Financial company data from a representative French population are reduced and projected onto a two-dimensional space with Uniform Manifold Approximation and Projection, a manifold learning algorithm. Former French funding recipients’ data are projected onto the two-dimensional space. Their distribution is non-uniform, with data concentrating in one region of the projection space. This region is identified using Density-based Spatial Clustering of Applications with Noise. Applicant companies which are projected within this region are labeled potential funding recipients and will be suggested the most competitive funding mechanisms

Software systems are ubiquitous, and their reliability is often crucial, especially for theones operating in embedded hardware, where the energetic sobriety moreover matters.To bring reliable guarantees, formal methods have been used for many years, with greatsuccess, among them automata based techniques and the renowned model checkingapproach. Instead of manually building a model, and verify it afterwards, anotherparadigm consists in automatically synthesising such correct by construction software,using game theory. Two players, the controller and an environment, are fighting oneagainst the other in a zero-sum game played on a graph of all possible configurations ofthe system. Energy, or other quantitative metrics of interest, are then modelled by theaddition of weights in the games. While some results have been obtained in the presenceof non-negative weights only, my objective has been to incorporate negative weights inthe picture, to model richer quantitative behaviours. This manuscript aims at studyinga combination of reachability objective with the total-payoff metrics, i.e. shortest-pathgames where one player wants to reach a target of the graph while minimising thecumulated weight. Our study starts with the case of finite graph games, with the searchfor efficient algorithms to compute optimal values and strategies. We then continue byadding clocks and time constraints in the games, in order to design efficient programssatisfying some real-time specifications. This leads to a notoriously difficult class ofgames where undecidability emerges very quickly. Our work consists into the search forfragments with decidable results, either by limiting the number of clocks, or the cyclicbehaviours in the game. A last chapter also studies the use of stochasticity in strategiesin order to limit the amount of memory needed for players to play optimally., Les systèmes logiciels sont omniprésents et leur fiabilité est souvent cruciale, en parti-culier pour ceux qui fonctionnent dans du matériel embarqué, où la sobriété énergétiqueest aussi un paramètre crucial. Pour apporter des garanties sûres, les méthodes formellessont utilisées depuis de nombreuses années, avec beaucoup de succès, avec entre autresdes techniques basées sur les automates et le célèbre model checking. Au lieu de créermanuellement un logiciel, son modèle et de vérifier celui-ci dans un deuxième temps, unautre paradigme consiste à synthétiser automatiquement un logiciel correct par construc-tion, en utilisant la théorie des jeux. Deux joueurs, le contrôleur et un environnement,s’affrontent dans un jeu à somme nulle joué sur un graphe de toutes les configurations dusystème. L’énergie, ou d’autres mesures quantitatives selon le problème envisagé, sontensuite modélisées par l’ajout de poids dans les jeux. Certains résultats préliminairesavaient été obtenus en présence de pondérations positives uniquement, mon objectif a étéd’autoriser l’usage de poids négatifs permettant de modéliser des données quantitativesplus riches. Ce manuscrit résume mes contributions dans l’étude d’une combinaison d’unobjectif d’accessibilité avec une métrique de gain total : on s’intéresse donc à des jeux deplus court chemin où un joueur veut atteindre une cible du graphe tout en minimisantle poids accumulé. Notre étude commence par le cas des jeux sur graphes finis, avec larecherche d’algorithmes efficaces pour calculer les valeurs et stratégies optimales. Nouscontinuons ensuite en ajoutant des horloges et des contraintes de temps dans les jeux,afin de concevoir des programmes efficaces satisfaisant certaines spécifications temps-réel.Cela conduit à une classe de jeux notoirement difficiles où l’indécidabilité émerge trèsrapidement. Notre travail consiste en la recherche de fragments possédant des résultatsdécidables, soit en limitant le nombre d’horloges, soit les comportements cycliques du jeu.Un dernier chapitre étudie également l’utilisation de randomisation dans les stratégiesafin de limiter la quantité de mémoire nécessaire pour que les joueurs jouent de manièreoptimale.

International audience; A large software system exists in different forms, as different variants targeting different business needs and users. This kind of systems is provided as a set of "independent" products and not as a "single-whole". Developers use ad-hoc mechanisms to manage variability. We defend a vision of software development where we consider an SPL architecture starting from which the architecture of each variant can be derived before its implementation. Indeed, each derived variant can have its own life. In this paper, we propose a novel approach for Software Architecture Product Line (SAPL) Engineering. It consists of, i) a generic process for recovering an SAPL model which is a product line of "software architectures" from large-sized variants. ii) a forward-engineering process that uses the recovered SAPL to derive new customized software architecture variants. The approach is firstly experimented on thirteen Eclipse variants to create a new SAPL. Then, an intensive evaluation is conducted using an existing benchmark which is also based on Eclipse IDE. Our results showed that we can accurately reconstruct such an SAPL and derive effectively pertinent variants. Our study provides insights that recovering SAPL and then deriving software architectures offers good documentation to understand the software before changing it.

International audience; Polynomial Interrupt Timed Automata (PolITA) are finite automata with clocks organized along hierarchical levels. These clocks are equipped with an interruption mechanism, well suited to the modeling of real-time operating systems. Moreover, transitions between states contain polynomial guards and updates. The reachability problem in this class is known to be in 2EXPTIME with a decision procedure based on the cylindrical algebraic decomposition. We improve this complexity to EXPSPACE mainly using a combinatorial argument and we include a reduction leading to a PSPACE lower bound.

National audience; Il est courant d'utiliser les méthodes d'apprentissage automatique pour développer des modèles de pronostics précis et fiables permettant d'établir une classification des patients atteints d'une certaine maladie. La classification des patients, permet de regrouper les individus en fonction de leurs besoins et donc d'adapter le traitement du patient de manière pertinente. La disponibilité récente de données de patients atteints de la SLA (Sclérose Latérale Amyotrophique) a permis l'étude de différentes méthodes de pronostic et de classification. Certaines de ces méthodes d'apprentissage automatique ont réussi à exploiter les corrélations présentes dans les données pour mieux comprendre la progression de la maladie. Cependant, la quantité d'informations, c'est-à-dire le nombre de variables associées à un patient, peut perturber l'apprentissage car certaines variables ne sont pas pertinentes. Il est donc nécessaire de sélectionner un sous-ensemble des variables les plus appropriées de sorte à maximiser la qualité prédictive du modèle. La difficulté de cette stratégie est qu'elle est confrontée au problème de l'explosion combinatoire. En effet, le nombre de combinaisons possibles étant exponentiel, une énumération complète des sous-ensembles n'est pas réaliste. L'utilisation de méthodes statistiques et/ou de métaheuristiques permet d'approcher la solution optimale. De plus, un sous-ensemble de variables pourra mener à des performances différentes en fonction de la méthode d'apprentissage choisie (Régression logistique, Random forest, etc.). Le choix de la méthode d'apprentissage est généralement réalisé expérimentalement. La question est donc de déterminer, pour un jeu de données, le meilleur couple (métaheuristique, méthode d'apprentissage) permettant de maximiser la qualité prédictive du modèle obtenu.Dans ce travail, nous effectuons une comparaison expérimentale de 7 métaheuristiques parmi les plus courantes (algorithmes génétiques, recuit simulé, essaim de particules, etc.) afin de déterminer le meilleur sous-ensemble de variables. Nous les associons avec 9 méthodes d'apprentissage parmi les plus courantes. Chaque couple (métaheuristique, méthode) est appliqué sur 13 jeux de données benchmarks ainsi que sur des jeux de données provenant du domaine médical, pour un total de 945 expériences.Nos expériences semblent indiquer que les métaheuristiques sont plus efficaces que les méthodes statistiques puisque nous arrivons à obtenir un meilleur score sur 11 des 13 jeux de données. L'amélioration de la qualité prédictive peut aller jusqu'à 8 points. Nous avons appliqué notre méthodologie sur les données de patients atteints de la SLA. Nous obtenons une classification bien meilleure que dans, permettant ainsi une meilleure prise en charge des patients atteints de la SLA. Pour chacun de nos jeux de données la métaheuristique qui nous permet d'obtenir le meilleur résultat est une métaheuristique à base de population. En particulier, l'évolution différentielle semble être la métaheuristique la plus efficace. Les métaheuristiques à base de parcours semblent au contraire inadaptées. Les performances des métaheuristiques à base de population semblent décorrélées du choix de la méthode d'apprentissage. A partir de ces expériences, nous recommandons d'utiliser l'évolution différentielle pour sélectionner un sous-ensemble de variables, quelle que soit la méthode d'apprentissage utilisée.

The Kleene theorem establishes a fundamental link between automata and expressions over the free monoid. Numerous generalisations of this result exist in the literature; on one hand, lifting this result to a weighted setting has been widely studied. On the other hand, beyond the free monoid, different monoids can be considered: for instance, two-way automata, and even tree-walking automata, can be described by expressions using the free inverse monoid. In the present work, we aim at combining both research directions and consider weighted extensions of automata and expressions over a class of monoids that we call pre-rational, generalising both the free inverse monoid and graded monoids. The presence of idempotent elements in these pre-rational monoids leads in the weighted setting to consider infinite sums. To handle such sums, we will have to restrict ourselves to rationally additive semirings. Our main result is thus a generalisation of the Kleene theorem for pre-rational monoids and rationally additive semirings. As a corollary, we obtain a class of expressions equivalent to weighted two-way automata, as well as one for tree-walking automata., LIPIcs, Vol. 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), pages 6:1-6:16

While the complexity of translating future linear temporal logic (LTL) into automata on infinite words is well-understood, the size increase involved in turning automata back to LTL is not. In particular, there is no known elementary bound on the complexity of translating deterministic $\omega$-regular automata to LTL. Our first contribution consists of tight bounds for LTL over a unary alphabet: alternating, nondeterministic and deterministic automata can be exactly exponentially, quadratically and linearly more succinct, respectively, than any equivalent LTL formula. Our main contribution consists of a translation of general counter-free deterministic $\omega$-regular automata into LTL formulas of double exponential temporal-nesting depth and triple exponential length, using an intermediate Krohn-Rhodes cascade decomposition of the automaton. To our knowledge, this is the first elementary bound on this translation. Furthermore, our translation preserves the acceptance condition of the automaton in the sense that it turns a looping, weak, B\"uchi, coB\"uchi or Muller automaton into a formula that belongs to the matching class of the syntactic future hierarchy. In particular, it can be used to translate an LTL formula recognising a safety language to a formula belonging to the safety fragment of LTL (over both finite and infinite words)., Comment: Full version with appendix of a chapter with the same title that appears in the FoSSaCS 2022 conference proceedings

International audience; Zielonka's classic recursive algorithm for solving parity games is perhaps the simplest among the many existing parity game algorithms. However, its complexity is exponential, while currently the state-of-the-art algorithms have quasipolynomial complexity. Here, we present a modification of Zielonka's classic algorithm that brings its complexity down to $n^{\mathcal{O}\left(\log\left(1+\frac{d}{\log n}\right)\right)}$, for parity games of size $n$ with $d$ priorities, in line with previous quasipolynomial-time solutions.

International audience; Identifying patterns in the modus operandi of attackers is an essential requirement in the study of Advanced Persistent Threats. Previous studies have been hampered by the lack of accurate, relevant, and representative datasets of current threats. System logs and network traffic captured during attacks on real companies' information systems are the best data sources to build such datasets. Unfortunately, for apparent reasons of companies' reputation, privacy, and security, such data is seldom available. This article proposes an alternative approach to such issues involved with collecting data. It first presents a formal model of an attacker's tactical progression during their network propagation phase. Such a progression is expressed according to the attacker's state, called muSE, which specifies their propagation area, collected secrets, and knowledge of the environment. The new model wields the operational semantics of attack techniques proposed in this article. The semantics formally define a transition relation between attackers' states. Hence, it can be used to describe an entire attack scenario. This formalization allows the ability to describe the PWNJUTSU experiment unequivocally. In this experiment, 22 Red Teamers attacked the vulnerable infrastructure to compromise machines and steal secret flags. Each Red Teamer operated on a dedicated instance. Sensors captured system logs and network traffic on each of these instances. This article's second contribution is the public release of the PWNJUTSU dataset.

International audience; Epidemiological models become more and more complex as new concerns are taken into account (age, sex,spatial heterogeneity, containment or vaccination policies, etc.). This is problematic because these aspects aretypically intertwined which makes models difficult to extend, change or reuse. The Kendrick approach hasshown promising results to separate epidemiological concerns but is restricted to homogeneous compartmentalmodels. In this paper, we report on an attempt to generalize the Kendrick approach to support some aspectsof contact networks, thereby improving the predictive quality of models with significant heterogeneity in thestructure of contacts, while keeping the simplicity of compartmental models. This approach has been validatedon two different techniques to generalize compartmental models.

We explore the notion of history-determinism in the context of timed automata (TA). History-deterministic automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and history-deterministic specifications allow for game-based verification without an expensive determinization step. We show yet another characterisation of history-determinism in terms of fair simulation, at the general level of labelled transition systems: a system is history-deterministic precisely if and only if it fairly simulates all language smaller systems. For timed automata over infinite timed words it is known that universality is undecidable for Büchi TA. We show that for history-deterministic TA with arbitrary parity acceptance, timed universality, inclusion, and synthesis all remain decidable and are ExpTime-complete. For the subclass of TA with safety or reachability acceptance, we show that checking whether such an automaton is history-deterministic is decidable (in ExpTime), and history-deterministic TA with safety acceptance are effectively determinizable without introducing new automata states., LIPIcs, Vol. 243, 33rd International Conference on Concurrency Theory (CONCUR 2022), pages 14:1-14:21

The evolution of classical information systems has introduced new technologies and services forinformation managing and sharing. With the spread of the Internet, it is now possible to easilyshare vast amounts of electronic information and computer resources in open distributed envi-ronments. These environments serve as a common platform for heterogeneous users by hostingservices, user applications and data. This evolution has opened new threats to informationsecurity and new challenges to access control modeling. In order to meet these challenges,many research works went towards extending traditional access control models towards mod-els tailored for managing data access and privilege definition within distributed and dynamicsystems.In this manuscript, we contribute to this line of research by introducing a modular frameworkfor the specification of interoperable access control policies developed autonomously in differentadministrative domains. The rule-based formalisation we propose allows for policy analysis andvalidation by verification of policy properties and simulation of execution scenarios. We havealso investigated access control in the context of collaborative decision making systems. In par-ticular, we propose a solution for controlling access in cooperating web services with transitivedependencies, as well as in data fusion processes. Finally, we consider authorization policiesand constraints related to workflow management systems and workflow-driven applications.We propose a methodology to monitor a workflow and its associated access control policy inorder to ensure a successful termination of the workflow or, if not possible, an execution witha minimal violation of the authorization constraints., L’evolution des systemes d’information classiques a introduit des nouvelles technologies et desnouveaux services pour la gestion et le partage d’informations. Avec la diffusion d’Internet, ilest desormais possible de partager facilement de grandes quantites d’informations ́electroniqueset de ressources informatiques dans des environnements distribues ouverts. Ces environnementsservent de plateforme commune pour des utilisateurs heterogenes (par exemple, les entreprises,les particuliers, etc.) en h ́ebergeant des services, des applications utilisateur et des donn ́ees.Cette evolution a introduit des nouvelles menaces pour la s ́ecurit ́e de l’information et desnouveaux d ́efis pour la modelisation du contrˆole d’acc`es. Afin de relever ces d ́efis, de nombreuxtravaux de recherche etudient l’extension des mod`eles traditionnels de contrˆole d’acc`es vers desmod`eles con ̧cus pour gerer l’acces aux donn ́ees et la d ́efinition des privil`eges dans les syst`emesdistribu ́es et dynamiques.Dans ce manuscrit, nous contribuons `a cette ligne de recherche en introduisant un formalismepour la sp ́ecification de politiques de contrˆole d’acc`es interop ́erables et d ́evelopp ́ees de mani`ereautonome dans diff ́erents domaines administratifs. La formalisation `a base de r`egles que nousproposons permet l’analyse et la validation des politiques par la v ́erification des propri ́et ́estelles que la consistance et l’efficacit ́e, ainsi que la simulation de sc ́enarios d’ex ́ecution. Nousavons ́egalement ́etudi ́e le contrˆole d’acc`es dans le contexte des syst`emes avec une prise ded ́ecision collaborative. Nous proposons notamment une solution pour le contrˆole d’acc`es dansles services web cooperatifs avec des dependances transitives, ainsi que dans les processus defusion de donnees.Enfin, nous considerons les politiques d’autorisation et les contraintes liees aux systemes degestion de flux de travail (workflows) et leurs applications. Nous proposons une methodologiepour surveiller un workflow et sa politique de controle d’acces associee, afin d’en assurer laterminaison en respectant toutes les contraintes de securite ou, si ce n’est pas possible, uneexecution avec une violation minimale de ces contraintes.

International audience; Monitorability is a characteristic that delineates between the properties that can be runtime verified by a monitor and those that cannot. Existing notions of monitorability for branching-time specifications are quite restrictive, limiting the set of monitorable properties to a small logical fragment. A recent study has enlarged the set of monitorable branching-time properties by weakening the requirements expected of the monitors effecting the verification: it defines a novel notion of optimal monitor that carries out the maximum number of detections that can be effected for any property, thereby turning a branching-time property into a monitorable one. The study also outlines a method for obtaining a unique optimal monitor from any branching-time property but falls short of providing an automation for this procedure. In this paper, we present a prototype tool that generates monitorable properties for branchingtime properties expressed in a variant of the modal μ-calculus, based on this procedure. We also assess the performance of the prototype tool by evaluating its performance against several specifications.

International audience; BPMN is the standard for business process modeling. It includes a rich set of constructs for control-flow, inter-process communication, and time-related concerns. However, spatial concerns are left apart while being essential to several application domains. We propose a comprehensive extension of BPMN to deal with this. Our proposal includes an integrated notation, a first-order logic semantics of the extension, and tool-supported verification means through the implementation of the semantics in TLA . Our tool support and our model database are open source and freely available online.

Automata models between determinism and nondeterminism/alternations can retain some of the algorithmic properties of deterministic automata while enjoying some of the expressiveness and succinctness of nondeterminism. We study three closely related such models - history determinism, good for gameness and determinisability by pruning - on quantitative automata. While in the Boolean setting, history determinism and good for gameness coincide, we show that this is no longer the case in the quantitative setting: good for gameness is broader than history determinism, and coincides with a relaxed version of it, defined with respect to thresholds. We further identify criteria in which history determinism, which is generally broader than determinisability by pruning, coincides with it, which we then apply to typical quantitative automata types. As a key application of good for games and history deterministic automata is synthesis, we clarify the relationship between the two notions and various quantitative synthesis problems. We show that good-for-games automata are central for "global" (classical) synthesis, while "local" (good-enough) synthesis reduces to deciding whether a nondeterministic automaton is history deterministic., LIPIcs, Vol. 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021), pages 38:1-38:20

International audience; The future intelligent manufacturing systems should possess a high degree of autonomy, which is able to monitor the entire production process, quickly re-plan operations, and respond to various unforeseen situations in a secure and safe manner. This can achieve rapid response to customers and avoid costly machine downtime, which is crucial to maintaining business success and profitability. The Asset Administration Shell (AAS) is an emerging standard in the I4.0 (Industry 4.0) domain. Based on the concept of digital twins, it provides concepts for describing the digital representation of I4.0 assets including their capabilities and skills. The AAS provides also responses to the challenge of syntactic and semantic interoperability that the flexible and autonomous production lines are facing. In this article, we propose a capability-based operation and engineering approach for flexible production lines. Our approach is relying on the AAS standard which is a very wide and rich specification. Consequently, we describe the subset of AAS modelling concepts necessary for our approach, we clarify their semantics and we show their usage through a production cell use case. Furthermore, we demonstrate how these modelling concepts were tooled as an extension of the open source model-driven workbench Papyrus.

International audience; Lot-size-one systems as well as plug and produce concepts imply (1) producing increased variety of products in a highly flexible and timely manner, and (2) making commissioning and maintenance more flexible. The speed with which manufacturers, in particular SMEs, can reconfigure the production to a new run and thus respond to clients and avoid costly machine downtime is critical to maintaining commercial success and profit margins. The manufacturing systems of tomorrow must offer a high degree of autonomy, be quickly re-planned to other operations, and cope with a wide variety of unforeseen situations, in a secure and safe manner. In this context, the Asset Administration Shell (AAS) is an emergent standard that leverages the digital twin approach and provides concepts for describing capabilities and skills of I4.0 components in order to automate the reconfiguration process. This article proposes a capability-based operation and engineering approach to tackle the syntactic and semantic interoperability problems in flexible production lines. We demonstrate the implementation of the AAS standard in the open source model-driven workbench Papyrus; then we assess its usability for modeling a production cell use case in order to implement a capability-based reconfiguration approach for flexible production lines.

International audience; In this paper, we consider a symbolic mechanism designed to help guide the performance of actions of a Belief-Desire-Intention (BDI) agent under both concurrency and relevance criteria. Behind the planning activity which can optimistically estimate the relevance of traces, we propose to directly supervise the best effort execution of the intentions as to keep track of the most relevant ones in case of failures. To support the presented method, a typical use case is given that targets the automated guidance of an autonomous vehicle.

The problem of distributed synthesis is to automatically generate a distributed algorithm, given a target communication network and a specification of the algorithm's correct behavior. Previous work has focused on static networks with an a priori fixed message size. This approach has two shortcomings: Recent work in distributed computing is shifting towards dynamically changing communication networks rather than static ones, and an important class of distributed algorithms are so-called full-information protocols, where nodes piggy-pack previously received messages onto current messages. In this work, we consider the synthesis problem for a system of two nodes communicating in rounds over a dynamic link whose message size is not bounded. Given a network model, i.e., a set of link directions, in each round of the execution, the adversary choses a link from the network model, restricted only by the specification, and delivers messages according to the current link's directions. Motivated by communication buses with direct acknowledge mechanisms, we further assume that nodes are aware of which messages have been delivered. We show that the synthesis problem is decidable for a network model if and only if it does not contain the empty link that dismisses both nodes' messages., Comment: In Proceedings GandALF 2020, arXiv:2009.09360

International audience; This book – composed of two volumes – explores the syntactical constructs of the most common programming languages, and sheds a mathematical light on their semantics, providing also an accurate presentation of the material aspects that interfere with coding.Concepts and Semantics of Programming Languages 2 presents an original semantic model, collectively taking into account all of the constructs and operations of modules and classes: visibility, import, export, delayed definitions, parameterization by types and values, extensions, etc. The model serves for the study of Ada and OCaml modules, as well as C header files. It can be deployed to model object and class features, and is thus used to describe Java, C++, OCaml and Python classes.This book is intended not only for computer science students and teachers but also seasoned programmers, who will find a guide to reading reference manuals and the foundations of program verification.

Weighted timed games are two-player zero-sum games played in a timed automaton equipped with integer weights. We consider optimal reachability objectives, in which one of the players, that we call Min, wants to reach a target location while minimising the cumulated weight. While knowing if Min has a strategy to guarantee a value lower than a given threshold is known to be undecidable (with two or more clocks), several conditions, one of them being the divergence, have been given to recover decidability. In such weighted timed games (like in untimed weighted games in the presence of negative weights), Min may need finite memory to play (close to) optimally. This is thus tempting to try to emulate this finite memory with other strategic capabilities. In this work, we allow the players to use stochastic decisions, both in the choice of transitions and of timing delays. We give for the first time a definition of the expected value in weighted timed games, overcoming several theoretical challenges. We then show that, in divergent weighted timed games, the stochastic value is indeed equal to the classical (deterministic) value, thus proving that Min can guarantee the same value while only using stochastic choices, and no memory., LIPIcs, Vol. 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), pages 137:1-137:17

Supervised learning models are usually trained on data with limited constraints. Unfortunately, data are generally scarce, incomplete and biased in real-world use cases, which hampers efficient model design. Such data can and should still be leveraged to discover relevant patterns, glean insight and develop meaningful conclusions. In this thesis, we investigate an unsupervised learning approach to isolate minority samples encompassed within a larger population. Our review includes two different use cases: Amyotrophic Lateral Sclerosis prognosis and identification of potential innovation funding recipients. Despite differences in their purpose, these contexts face similar issues: poor data availability of partial and unrepresentative samples. In both cases, the aim is to detect samples from a minority population: patients with a poorer 1-year prognosis and companies that are more likely to be successful funding applicants. Data are projected into a lower-dimensional space using Uniform Manifold Approximation and Projection (UMAP), a nonlinear dimension reduction technique. Differences in data distributions are harnessed and used to isolate the target minority population, using Density Based Clustering of Applications with Noise (DBSCAN) and alpha shapes. Correlations between input and target variables become visible within the projection space and minority samples are isolated from the remaining data. As a result, in spite of poor data quality, we provide additional insight with regard to recently diagnosed patients and potential funding applicants.; Les modèles d'apprentissage supervisé sont généralement entraînés sur des données aux contraintes limitées. Malheureusement, les données sont souvent rares, incomplètes et biaisées dans de nombreux cas d’applications, et cela entrave la conception de modèles efficaces. De telles données peuvent et doivent néanmoins être exploitées, car elles demeurent des sources précieuses d’information. Elles permettent de découvrir des corrélations pertinentes et de parvenir à des conclusions significatives. Dans cette thèse, nous étudions une approche d'apprentissage non supervisé pour isoler des échantillons minoritaires compris à l’intérieur d’une population plus large. Notre étude intègre deux contextes applicatifs: le pronostic de la Sclérose Latérale Amyotrophique (SLA) et la recommandation aux entreprises de dispositifs publics de financement de l’innovation. Malgré des différences dans leur objectif, ces contextes sont confrontés à des problèmes similaires: une faible disponibilité des données associée à des échantillons non représentatifs et incomplets. Dans les deux cas, l'objectif est de détecter des échantillons d'une population minoritaire: les patients dont le pronostic à un an est défavorable et les sociétés qui ont plus de chances d'obtenir des financements. Les données sont projetées dans un espace bidimensionnel à l'aide de la méthode d’approximation et de projection de variété uniforme (UMAP), une technique de réduction de dimension non linéaire. Les différences de distribution des données sont exploitées de manière à isoler la population minoritaire cible, à l'aide du partitionnement spatial par densité (DBSCAN) et des formes alpha. Les corrélations entre les caractéristiques d'entrée et d’intérêt, que sont la survie à 1 an et l’obtention de financements, deviennent visibles dans l'espace de projection et les échantillons minoritaires sont isolés du reste des données. En dépit des contraintes sur les données, notre approche se révèle pertinente et informative au regard de patients récemment diagnostiqués avec la SLA et d'entreprises qui postulent pour un financement.

International audience; This paper presents detectEr, a runtime verification tool for monitoring asynchronous component systems. The tool synthesises executable monitors from properties expressed in terms of the safety fragment of the modal μ-calculus. In this paper, we show how a number of useful properties can be flexibly runtime verified via the three forms of instrumentation-inline, outline, and offline-offered by detectEr to cater for specific system setup constraints.

In various scientific communities dealing with formal analysis, software competitions have emerged and contributed to fostering progress in state of the art and providing insight into the evolution of the involved technologies. The model checking contest (MCC) is one of them; it focuses on asynchronous concurrent systems. This paper reports what the organizers have observed over five editions of the MCC between 2015 and 2019. It shows the evolution of state-of-the-art model checking tools in performing large and difficult verification tasks by improving existing techniques or designing new and innovative (combinations of) techniques. This paper also shows the impact of such an event on the corresponding scientific community.

We study the expressiveness and succinctness of good-for-games pushdown automata (GFG-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of the remainder of the input word. We prove that GFG-PDA recognise more languages than deterministic PDA (DPDA) but not all context-free languages (CFL). This class is orthogonal to unambiguous CFL. We further show that GFG-PDA can be exponentially more succinct than DPDA, while PDA can be double-exponentially more succinct than GFG-PDA. We also study GFGness in visibly pushdown automata (VPA), which enjoy better closure properties than PDA, and for which we show GFGness to be ExpTime-complete. GFG-VPA can be exponentially more succinct than deterministic VPA, while VPA can be exponentially more succinct than GFG-VPA. Both of these lower bounds are tight. Finally, we study the complexity of resolving nondeterminism in GFG-PDA. Every GFG-PDA has a positional resolver, a function that resolves nondeterminism and that is only dependant on the current configuration. Pushdown transducers are sufficient to implement the resolvers of GFG-VPA, but not those of GFG-PDA. GFG-PDA with finite-state resolvers are determinisable., LIPIcs, Vol. 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021), pages 53:1-53:20

International audience; This book – the first of two volumes – explores the syntactical constructs of the most common programming languages, and sheds a mathematical light on their semantics, while also providing an accurate presentation of the material aspects that interfere with coding.Concepts and Semantics of Programming Languages 1 is dedicated to functional and imperative features. Included is the formal study of the semantics of typing and execution; their acquisition is facilitated by implementation into OCaml and Python, as well as by worked examples. Data representation is considered in detail: endianness, pointers, memory management, union types and pattern-matching, etc., with examples in OCaml, C and C++. The second volume introduces a specific model for studying modular and object features and uses this model to present Ada and OCaml modules, and subsequently Java, C++, OCaml and Python classes and objects.This book is intended not only for computer science students and teachers but also seasoned programmers, who will find a guide to reading reference manuals and the foundations of program verification.

Interrupt Timed Automata ( ITA ) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA ( PolITA ). We prove that reachability is decidable in 2EXPTIME on PolITA , using an adaptation of the cylindrical algebraic decomposition algorithm for the first-order theory of reals. We also obtain decidability for the model checking of a timed version of CTL and for reachability in several extensions of PolITA . In particular, compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also study expressiveness questions for PolITA and show that PolITA are incomparable with stopwatch automata.

In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals (ω-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite. In this paper, we do not make such an assumption and consider data ω-words instead, i.e. words over an infinite alphabet. In this context, we study specifications and implementations respectively given as automata and transducers extended with a finite set of registers. We consider different instances, depending on whether the specification is nondeterministic, universal or deterministic, and depending on whether the number of registers of the implementation is given (bounded synthesis) or not.In the unbounded setting, we show undecidability for both universal and non-deterministic specifications, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but can be recovered by disallowing tests over input data. The generic technique we use to show the latter result allows us to reprove some known result, namely decidability of bounded synthesis for universal specifications., CONCUR 2019, info:eu-repo/semantics/inPress

International audience

Brute-force model-checking consists in exhaustive exploration of the state-space of a Petri net, and meets the dreaded state-space explosion problem. In contrast, this paper shows how to solve model-checking problems using a combination of techniques that stay in complexity proportional to the size of the net structure rather than to the state-space size. We combine an SMT based over-approximation to prove that some behaviors are unfeasible, an under-approximation using memory-less sampling of runs to find witness traces or counter-examples, and a set of structural reduction rules that can simplify both the system and the property. This approach was able to win by a clear margin the model-checking contest 2020 for reachability queries as well as deadlock detection, thus demonstrating the practical effectiveness and general applicability of the system of rules presented in this paper., Extended Journal version of ICATPN 2020 paper published in Fundamenta Informaticae

International audience; Ce livre s’adresse aux développeurs, concepteurs et intégrateurs de logiciels ainsi qu’aux chefs de projets et aux architectes.Avec la montée en charge du big data, et du cloud computing, la fiabilité des logiciels est plus importante que jamais. Concevoir du premier coup et sans aucune erreur un logiciel qui comporte plusieurs millions de lignes de code et plusieurs centaines de composants est évidemment impossible. La nécessité de faire des tests au cours des différentes phases de conception paraît évidente et pourtant, dans la pratique, les tests sont souvent négligés et relégués au second plan. L’objectif de cet ouvrage est triple :–– donner les bases et les bonnes pratiques pour concevoir et mener à bien des tests ;–– fournir un référentiel en termes de méthodes et de vocabulaire ;–– préparer la certification ISTQB du métier de testeur.Cette quatrième édition rend compte des évolutions dans la pratique des tests logiciels au cours des trois dernières années.

International audience; Copyless streaming string transducers (copyless SST) have been introduced by R. Alur and P. ˇ Cern´yCern´y in 2010 as a one-way determin-istic automata model to define transductions of finite strings. Copyless SST extend deterministic finite state automata with a set of variables in which to store intermediate output strings, and those variables can be combined and updated all along the run, in a linear manner, i.e., no variable content can be copied on transitions. It is known that copyless SST capture exactly the class of MSO-definable string-to-string trans-ductions, and are as expressive as deterministic two-way transducers. They enjoy good algorithmic properties. Most notably, they have decid-able equivalence problem (in PSpace). On the other hand, HDT0L systems have been introduced for a while, the most prominent result being the decidability of the equivalence problem. In this paper, we propose a semantics of HDT0L systems in terms of transductions, and use it to study the class of deterministic copyful SST. Our contributions are as follows: (i) HDT0L systems and total deterministic copyful SST have the same expressive power, (ii) the equivalence problem for deterministic copyful SST and the equivalence problem for HDT0L systems are inter-reducible, in linear time. As a consequence, equivalence of deterministic SST is decid-able, (iii) the functionality of non-deterministic copyful SST is decidable, (iv) determining whether a deterministic copyful SST can be transformed into an equivalent deterministic copyless SST is decidable in polynomial time.

National audience; Cet ouvrage explore les constructions syntaxiques des langages de programmation les plus courants, avec un éclairage mathématique sur leurs sémantiques et une présentation précise des aspects matériels qui interfèrent avec le codage.Ce deuxième volume présente un modèle sémantique original commun aux constructions et opérations des modules et des classes : visibilité, importation, exportation, définitions différées, paramétrisation par types et valeurs, extensions. Ce modèle fonde l’étude des modules d’Ada, OCaml et des fichiers d’en-tête de C. Il est décliné pour modéliser les traits objet puis utilisé pour traiter les classes de C++, Java, Python et OCaml.Concepts et sémantique des langages de programmation 2 s’adresse aux étudiants et enseignants des cursus informatiques ainsi qu’aux programmeurs chevronnés, qui y trouveront un guide de lecture des manuels de référence ainsi que les fondements de la vérification de programmes.