Programme des journées 2014#

Voir les informations locales pour trouver la salle 25-26/105 au lip6, Université P. et M. Curie, Jussieu.

Lundi 16 juin#

13:30–13:45
Accueil

13:45–14
Mots de bienvenue

14–15
Exposé invité (chair: Pierre-Cyrille Héam)
  • Serge Haddad, Diagnostic actif [abstract] [Slides]

    Le diagnostic consiste à détecter l'occurrence de fautes dans un système à événements discrets partiellement observable. Un tel système peut être diagnostiquable ou pas. Aussi le diagnostic actif vise à le contrôler afin de le rendre diagnostiquable. Aprés avoir formalisé le problème, nous décrirons d'abord des procédures de décision de complexité optimale et de synthèse de diagnostiqueur de taille optimale basées sur des techniques d'automates et de jeux. Puis nous étudierons ces mêmes problèmes dans un cadre probabiliste montrant que selon les exigences requises, le problème se situe d'un côté ou de l'autre de la frontière de la décidabilité. Lorsque les problèmes sont décidables, nous décrirons aussi des procédures optimales.

    Ce travail repose sur des collaborations avec Nathalie Bertrand, Eric Fabre, Stefan Haar, Loïc Hélouët, Tarek Melliti et Stefan Schwoon.

15–15:30
Pause café
15:30–16:45
Algorithmique distribuée (chair: Fabrice Kordon)
  • Marion Guthmuller et Martin Quinson, Vérification dynamique d'applications distribuées avec SimGridMC [abstract] [Slides]

    Notre travail s'inscrit dans le contexte de l'étude conjointe de la correction et de la performance d'applications distribuées, sans nécessiter de réécriture entre les modèles, algorithmes et implémentations réelles. Pour cela, nous nous appuyons sur l'environnement SimGrid, qui permet initialement de simuler des systèmes distribués à large échelle tels que les grilles, le Cloud, les applications HPC ou bien encore les systèmes P2P. Au sein de cet outil de simulation, nous proposons l'outil de vérification SimGridMC qui permet de vérifier dynamiquement (en exécutant et en vérifiant l'application réelle) les applications étudiées à travers le simulateur.

  • Philippe Merle, Vers une spécification formelle et outillée pour Open Cloud Computing Interface [abstract]

    L'informatique en nuage (ou Cloud Computing) permet aux utilisateurs de louer à la demande des ressources numériques (processeur, mémoire, stockage, réseau, pile logicielle, application en ligne, etc.) et de les administrer à distance. L'Open Cloud Computing Interface (OCCI) est un ensemble de spécifications de l'Open Grid Forum (OGF) définissant une interface ouverte, simple, extensible et auto-descriptive pour la gestion de ces ressources en nuage (http://occi-wg.org/). Cependant ces spécifications écrites en anglais restent informelles et donc potentiellement inconsistantes, ambigües et incomplètes. Notre objectif est de proposer une spécification formelle d'OCCI qui soit mathématiquement consistante, non ambigüe et complète.

    Nous avons choisi Alloy, un langage de spécification léger basé sur la logique relationnelle du premier ordre pour écrire notre spécification formelle d'OCCI. L'intérêt d'Alloy est la simplicité de ce langage et l'utilisation facile de son analyseur (http://alloy.mit.edu), qui agit essentiellement comme un vérificateur de modèles et un générateur de contre-exemples. Cela permet de rapides itérations entre modélisation et analyse lors de l'écriture et la mise au point d'une spécification. Cet exposé présentera une spécification en Alloy de la sémantique statique et d'une partie de la sémantique dynamique du coeur d'OCCI.

    Ce modèle formel est ensuite outillé dans l'environnement Eclipse par une chaîne d'outils dirigée par le modèle OCCI. Cette chaîne propose un langage dédié de modélisation OCCI. La syntaxe abstraite de ce langage est capturée via un méta-modèle Ecore, la syntaxe concrète est un schéma XMI (XML Modeling Interchange), la sémantique statique est exprimée par des contraintes OCL (Object Constraint Language) et la sémantique dynamique est programmée en Kermeta (http://www.kermeta.org). Enfin, notre chaîne offre un modeleur graphique pour modéliser des extensions OCCI.

  • Laure Millet, Maria Gradinariu Potop-Butucaru, Nathalie Sznadjer et Sébastien Tixeuil, On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering [abstract] [Slides]

    Recent advances in Distributed Computing highlight models and algorithms for autonomous swarms of mobile robots that self-organize and cooperate to solve global objectives. The overwhelming majority of works so far considers handmade algorithm and correctness proofs.

    This paper is the first to propose a formal framework to automatically design distributed algorithms that are dedicated to autonomous mobile robots evolving in a discrete space. As a case study, we consider the problem of gathering all robots at a particular location, not known beforehand. Our contribution is threefold. First, we propose an encoding of the gathering problem as a reachability game. Then, we automatically generate an optimal distributed algorithm for three robots evolving on a fixed size uniform ring. Finally, we prove by induction that the generated algorithm is also correct for any ring size except when an impossibility result holds (that is, when the number of robots divides the ring rize).

17–18
Discussions autour du GT-Vérif

Mardi 17 juin#

8:30–9
Accueil
9–10
Exposé invité (chair: Véronique Cortier)
  • Stephan Merz, TLAPS : une plate-forme pour les preuves formelles d'algorithmes répartis [abstract] [Slides]

    Le langage TLA+ est destiné à la spécification de systèmes et particulièrement d'algorithmes répartis. Il est fondé sur la théorie des ensembles pour modéliser les aspects statiques et sur la logique temporelle pour décrire les exécutions d'un système. Les principaux outils de vérification associés à TLA+ sont le model checker TLC et la plate-forme interactive de preuves TLAPS. Cette dernière repose sur un langage hiérarchique de preuve et intègre différents outils de preuve automatisés. L'exposé donnera un aperçu des choix qui ont été faits dans la conception du langage de preuve et de TLAPS, des défis concernant l'intégration d'outils externes, de quelques exemples d'application pour la vérification d'algorithmes et présentera des travaux en cours et à venir.

    Travail commun avec la participation de Kaustuv Chaudhuri, Denis Cousineau, Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Dan Ricketts et Hernán Vanzetto.

10–10:30
Pause café
10:30–12:10
Vérification et logique (chair: Stephan Merz)
  • Ala Eddine Ben Salem, Symbolic Model Checking of Stutter-invariant Properties Using Generalized Testing Automata [abstract] [Slides]

    In a previous work, we showed that a kind of ω-automata known as Transition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties.

    In this work, we investigate the use of these generalized testing automata to improve symbolic model checking of stutter-invariant LTL properties. We propose an efficient symbolic encoding of stuttering transitions in the product between a model and a TGTA. Saturation techniques available for decision diagrams then benefit from the presence of stuttering self-loops on all states of TGTA. Experimentation of this approach confirms that it outperforms the symbolic approach based on (transition-based) Generalized Buchi Automata.

  • Amira Methni, Belgacem Ben Hedia, Matthieu Lemerre, Serge Haddad et Kamel Barkaoui, Specifying and Verifying Concurrent C Programs with TLA+ [abstract]

    Verifying software systems automatically from their source code rather than manually modelling them in a dedicated language gives more confidence in establishing their properties. Here we propose a formal specification and verification approach for concurrent C programs directly based on the semantic of C. We define a set of translation rules and implement it in a tool (C2TLA+) that automatically translates C code into a TLA+ specification. The TLC model checker can use this specification to generate a model, allowing to check the absence of runtime errors and dead code in the C program in a given configuration. In addition, we present how to make the translated specification interact with manually written ones to: check the C code against safety or liveness properties; provide concurrency primitives or model hardware that cannot be expressed in C; and use abstract versions of translated C functions to address the state-explosion problem. We also show that we can verify refinement between this abstract version and the TLA+ specification obtained by translation. All these verifications have been conducted on an industrial case study, which is a part of the microkernel of the PharOS real-time system.

  • Yves-Stan Le Cornec et Franck Pommereau , Modular mu-calculus model-checking with formula-dependent hierarchical abstractions [abstract] [Slides]

    This paper defines a formal framework for the modular and hierarchical model-checking of μ-calculus against modular transitions systems. Given a formula φ, a module can be analysed alone, in such a way that the truth value of φ may be decided without the need to analyse other modules. If no conclusion can be drawn locally, the analysis provides information allowing to reduce the module to a smaller one that is equivalent with respect to the truth value of φ.

    This way, modules can be incrementally analysed, reduced and composed to other reduced modules until a conclusion is reached. On the one hand, modular analysis allows to avoid modules compositions and thus the corresponding combinatorial explosion; on the other hand, hierarchical analysis allows to reduce the modules that must be composed, which limits combi- natorial explosion. Moreover, by proposing three complementary formula-dependent reductions, we expect better reductions than general approaches like bisimulation or tau ∗ reductions. The current paper is focused on defining the theoretical tools for this approach; finding interesting strategies to apply them efficiently is left to future work.

  • Patrick Gardy, Temporal logic with sum and average assertions [abstract] [Slides]

    Extending formal verification techniques to handle quantitative aspects, both for the models and for the properties to be checked, has become a central research topic over the last twenty years. Following several recent works, we study model checking for (one-dimensional) weighted Kripke structures with positive and negative weights, and temporal logics constraining the total and/or average weight. We prove decidability when only accumulated weight is constrained, while allowing average-weight constraints alone already is undecidable.

12:10–13:30
Repas
13:30–15:10
Compteurs (chair: Sylvain Schmitz)
  • Michael Blondin, Alain Finkel et Pierre Mckenzie, Handling Infinitely Branching WSTS [abstract] [Slides]

    Well-structured transition systems (WSTS) as a general class of infinite-state systems have spawned decidability results for important problems such as termination, boundedness, control-state maintainability and coverability. WSTS consist of a (usually infinite) well ordered set of states, together with a monotone transition relation. WSTS have found multiple uses: in settling the decidability status of reachability and coverability for graph transformation systems, in the forward analysis of depth-bounded processes, in the verification of parameterized protocols and the verification of multi-threaded asynchronous software.

    Most decidability results concerning WSTS apply to the finitely branching variant. Yet some models (inserting automata, ω-Petri nets, ...) are naturally infinitely branching. Here we develop tools to handle infinitely branching WSTS by exploiting the crucial property that in the (ideal) completion of a well-quasi-ordered set, downward-closed sets are finite unions of ideals. Then, using these tools, we derive decidability results and we delineate the undecidability frontier in the case of the termination, the control-state maintainability and the coverability problems. A new forward algorithm for deciding coverability is obtained and boundedness is also shown decidable.

  • Christoph Haase, Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy [abstract] [Slides]

    I will show that for any fixed i>0, the Sigma-(i+1)-fragment of Presburger arithmetic, i.e., its restriction to i+1 quantifier alternations beginning with an existential quantifier, is complete for the i-th level of the weak EXP hierarchy. This result completes the computational complexity landscape for Presburger arithmetic, a line of research which dates back to the seminal work by Fischer & Rabin in 1974. Moreover, I will discuss bounds on sets of naturals definable in the existential fragment of Presburger arithmetic: given an existential formula p(x), I will show that the set of solutions is an ultimately periodic set whose period can be doubly-exponentially bounded from below and above.

    An online version of the paper is available from: http://arxiv-web3.library.cornell.edu/abs/1401.5266

  • Vincent Penelle, Jérôme Leroux et Grégoire Sutre, The Context-Freeness Problem is coNP-complete for Flat Counter Systems [abstract] [Slides]

    In this talk, we investigate a sub-problem of the stratifiability of semilinear sets - namely the semilinear sets that are given as finite systems of linear inequalities - and show that stratifiability is coNP-complete in this case. We then apply this result to flat counter systems.

  • Simon Halfon, Integer Vector Addition Systems with States [abstract] [Slides]

    This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of counters ranging over the integers. Even though it is folklore that reachability in ZVASS is NP-complete, it turns out that despite their naturalness this class has received little attention in the literature. We fill this gap by providing an in-depth analysis of the computational complexity of the aforementioned decision problems. Most interestingly, it turns out that while the addition of reset operations to ordinary VASS leads to undecidability and Ackermann-hardness of reachability and coverability, respectively, they can be added to ZVASS while retaining NP-completness of both coverability and reachability.

15:10–15:30
Pause café
15:30–16:45
Sécurité (chair: Catalin Dima)
  • Béatrice Berard et Olivier Carton, Channel Synthesis Revisited [abstract] [Slides]

    Given a system modeled by a rational relation R, a channel is a pair (E,D) of rational relations that respectively encode and decode binary messages, and such that the composition E R D is the identity relation. This means that the message between E and D has been perfectly transmitted through R. Investigating the links between channels and the growth of rational sets of words, we give new characterizations for relations with channels. In the particular case where the relation is given as a union of functions, we obtain as a consequence the decidability of the synthesis problem with a linear complexity.

  • Quentin Monnet, Mathieu Sassolas et Lynda Mokdad, Modeling DoS Attacks in WSNs with quantitative games [abstract] [Slides]

    We use quantitative games with both energy and mean-payoff to model a network of wireless sensors where some nodes might be corrupted. (See file for extended abstract.)

  • Véronique Cortier et Cyrille Wiedling, A type libray for electronic voting protocols [abstract] [Slides]

    Many systems have been proposed for electronic voting during the past few years and some of them are very complex, involving e.g. a lot of cryptographic primitives to ensure security and usability for the voters. A secure voting system should ensure properties such as privacy, individual and universal verifiability, correctness, etc. Verifying that these complex protocols satisfy such properties can be tedious and many of the existing approaches often involve a lot of handwork leading to error-prone proofs. Automatic tools dedicated to security protocols may sometimes simplify the work but they have some limits and e-voting protocols are, for most of them, a few steps away from their scope.

    One major difficulty for automatic tools is that most electronic voting systems involve associative and commutative properties. Even though such properties are quite simple, they often lead to issues such as non termination. On the other hand, this kind of properties is handled very well by SMT solvers, used by type-systems. From this idea, we propose a type system to prove privacy-like properties. More precisely, based on a recent work from C. Fournet and al. on rF*, we develop a type system that can be applied to verify some e-voting protocols like Helios and a Norwegian E-voting protocol. This involves the development of a cryptographic library that could also be used to model and verify other system, automatically.


18h
À noter : à 18h et toujours à Jussieu (Amphithéâtre 15), colloque de Donald Knuth
20–23
Dîner au Bouillon Racine, 3 rue Racine, Paris 6e

Mercredi 18 juin#

8:30–9
Accueil
9–10
Exposé invité (chair: Didier Lime)
  • Eugene Asarin, Information dans les systèmes temporisés [abstract] [Slides]

    La notion centrale de cet exposé sera l’entropie d’un langage temporisé - un nombre réel qui caractérise la taille du langage et la quantité d’information (en bits par événement) dans ses mots. Après avoir justifié et défini l’entropie, j’expliquerai comment elle peut être calculée pour les langages des automates temporisés probabilistes. Je montrerai comment l’entropie rend possible la distinction entre les « mauvais » (Zéno, fragiles) automates temporisés et les « bons ». Je terminerai par une ébauche d’application à la transmission de l’information temporisée.

    Les résultats de l’exposé, publiés dans plusieurs articles, ont été obtenus avec N.Basset, M.-P. Béal, A.Degorre et D. Perrin.

10–10:30
Pause café
10:30–12:10
Jeux, synthèse, contrôle (chair: Eugene Asarin)
  • Nicolas Basset, Clemens Wiltsche et Marta Kwiatkowska, Compositional Controller Synthesis for Stochastic Games [abstract]

    Design of autonomous systems is facilitated by automatic synthesis of correct-by-construction controllers from formal models and specifications. We focus on stochastic games, which can model the interaction with an adverse environment, as well as probabilistic behaviour arising from uncertainties. We propose a synchronising parallel composition for stochastic games that enables a compositional approach to controller synthesis. We show how to leverage rules for compositional assume-guarantee verification of probabilistic automata to synthesise controllers for games with multi-objective quantitative winning conditions. By composing winning strategies synthesised for the individual components, we can thus obtain a winning strategy for the composed game, achieving better scalability and efficiency at a cost of restricting the class of controllers.

  • Rodica Bozianu, Catalin Dima et Emmanuel Filiot, Safraless Synthesis for Epistemic Temporal Specifications [abstract] [Slides]

    In this paper we address the synthesis problem for specifications given in linear temporal single-agent epistemic logic, KLTL (or KL_1), over single-agent systems having imperfect information of the environment state. Van der Meyden and Vardi have shown that this problem is 2Exptime complete. However, their procedure relies on complex automata constructions that are notoriously resistant to efficient implementations as they use Safra-like determinization. We propose a "Safraless" synthesis procedure for a large fragment of KLTL. The construction transforms first the synthesis problem into the problem of checking emptiness for universal co-Büchi tree automata using an information-set construction. Then we build a safety game that can be solved using an antichain-based symbolic technique exploiting the structure of the underlying automata. The technique is implemented and applied to a couple of case studies.

  • C. Aiswarya, Paul Gastin et K. Narayan Kumar, Controllers for the Verification of Communicating Multi-Pushdown Systems [abstract]

    Multi-pushdowns communicating via queues are formal models of multi-threaded programs communicating via channels. They are Turing powerful and much of the work on their verification has focused on under-approximation techniques. Any error detected in the under-approximation implies an error in the system. However the successful verification of the under-approximation is not as useful if the system exhibits unverified behaviours. One way to utilise the verification of an under-approximation is to restrict the system using a controller to stay within the under-approximation. We discuss some important properties that a good controller should satisfy. We consider an extensive under-approximation class, construct a distributed controller with the desired properties and also establish the decidability of verification problems for this class.

  • Axel Haddad, Benjamin Monmege, Gilles Geeraerts et Thomas Brihaye, Reachability-Cost Games with Negative Weights [abstract] [Slides]

    Reachability-cost games are two-player zero-sum games played on directed graphs with weights on edges, where two players take turns to choose transitions in order to optimize the total cost to reach a target set of vertices. More precisely, Player 1 wants to reach the target by minimizing its cost, whereas Player 2 wants to avoid the target, or, if not possible, maximize the cost of Player 1. When weights of edges are non-negative, polynomial algorithms are known in order to compute optimal values as well as optimal strategies for both players, see, e.g., an adaptation of Dijkstra's shortest path algorithm by Khachiyan et al. Moreover, both players are known to have optimal memoryless strategies. The case where weights can be any integer is more complex, especially in the presence of negative cycles. Filiot, Gentilini and Raskin prove that deciding whether the value of such a game is positive can be done in NP inter co-NP, by using methods similar to the one used for mean-payoff games: this holds even though optimal strategies may require memory, contrary to the nonnegative case. Our contribution is threefold. First, we present a value iteration algorithm to compute the optimal values, as well as optimal strategies for both players when they exist. This iterative algorithm has a pseudo-polynomial complexity (i.e., polynomial if weights of edges are encoded in unary). We also show that Player 2 always has optimal memoryless strategies and that a memory of size pseudo-polynomial is sufficient (and sometimes necessary) for Player 1. Finally, we show that deciding whether the value of the game is minus infinity (that is Player 1 has a family of strategies to secure a cost as small as possible) is as hard as solving mean-payoff games.

12:10–13:30
Repas
13:30–14:45
Robustesse (chair: Béatrice Bérard)
  • Loïc Helouët, S. Akshay, Pierre-Alain Reynier et Claude Jard, Robustness of Time Petri Nets under Guard Enlargement [abstract] [Slides]

    Robustness of timed systems aims at studying whether infinitesimal perturbations in clock values can result in new discrete behaviors. A model is robust if the set of discrete behaviors is preserved under arbitrarily small (but positive) perturbations. We tackle this problem for time Petri nets (TPNs, for short) by considering the model of parametric guard enlargement which allows time-intervals constraining the firing of transitions in TPNs to be enlarged by a (positive) parameter.

    We show that TPNs are not robust in general and checking if they are robust with respect to standard properties (such as boundedness, safety) is undecidable. We then extend the marking class timed automaton construction for TPNs to a parametric setting, and prove that it is compatible with guard enlargements. We apply this result to the (undecidable) class of TPNs which are robustly bounded (i.e., whose finite set of reachable markings remains finite under infinitesimal perturbations): we provide two decidable robustly bounded subclasses, and show that one can effectively build a timed automaton which is timed bisimilar even in presence of perturbations. This allows us to apply existing results for timed automata to these TPNs and show further robustness properties.

    This work is a joint work with S. Akshay and P.A. Reyniers. It was funded by the IMPRO ANR, and was originally published in the RP'2012 conference.

  • Nathalie Bertrand, Serge Haddad et Engel Lefaucheux, Specification and Verification of Diagnosis and Predictability in Probabilistic Systems [abstract] [Slides]

    In discrete event systems prone to unobservable faults, a diagnoser must eventually detect fault occurrences. The diagnosability problem consists in de- ciding whether such a diagnoser exists. Here we investigate diagnosis issues in a probabilistic framework modelled by partially observed Markov chains (or equivalently probabilistic labeled transition systems, denoted pLTS). First, we study different specifications of diagnosability and establish their relations both in finite and infinite pLTS. Then, we analyze the complexity of the diagnosability problem for finite pLTS: we show that the polynomial time procedure earlier proposed is erroneous, and that in fact for all considered specifications, the diagnosability problem is PSPACE-complete. We also establish exponential tight bounds for the size of diagnosers. Afterwards, we consider the alternative notion of predictability, aimed at anticipating faults. Predictability is easier than diag- nosability: it is NLOGSPACE-complete, yet the predictor synthesis is as hard as the diagnoser synthesis. Since predictability is more difficult to achieve than diagnosability, we finally introduce and study the more flexible notion of prediagnosability. Prediagnosers somehow combine the advantages of diagnosers and predictors, and we show that prediagnosability is a PSPACE-complete problem.

  • Youssouf Oualhadj, Pierre-Alain Reynier et Ocan Sankur, Probabilistic Robust Timed Games [abstract]

    Solving games played on timed automata is well-known and has led to tools and industrial case studies. In these games, the first player Controller chooses delays and actions and the second player Perturbator resolves the non-determinism of actions. However, the model of timed automata suffers from mathematical idealizations such as infinite precision of clocks and instantaneous synchronization of actions. To address this issue, we extend the theory of timed games in two directions. First, we study the synthesis of robust strategies for Controller which should be tolerant to adversarially chosen clock imprecisions. Second, we address the case of a stochastic perturbation model where both clock imprecisions and the non-determinism are resolved randomly. These notions of robustness guarantee the implementability of synthesized controllers. We provide characterizations of the resulting games for Büchi conditions, and prove the EXPTIME-completeness of the corresponding decision problems.

14:45–15:15
Pause café
15:15–16:30
Vérification et paramètres (chair: Serge Haddad)
  • Étienne André, Fabrice Kordon, Alban Linard et Laure Petrucci, CosyVerif, une plateforme pour la valorisation et l’enseignement des méthodes formelles [abstract] [Slides]

    CosyVerif est un environnement logiciel dédié à l’intégration d’outils de vérification formelle développé conjointement par les laboratoires LIP6, LIPN et LSV. L’objectif de cet environnement est double. Il permet de valoriser des résultats de recherche sous la forme d’outils logiciels opérationnels, permettant ainsi de les exposer à une exploitation pour résoudre des études de cas (y compris industrielles). Il peut également être utilisé comme outil d’enseignement en offrant une interface conviviale aux étudiants pour la réalisation de travaux pratiques.

    Cet exposé présentera CosyVerif, ses applications, son architecture, ses fonctionnalités, et fera le point sur son utilisation, en particulier en enseignement tant à l’UPMC qu’à L’UP13.

  • Benedikt Bollig, Paul Gastin et Jana Schubert, Parameterized Verification of Communicating Automata under Context Bounds [abstract] [Slides]

    We study the verification problem for parameterized communicating automata (PCA), in which processes synchronize via message passing. A given PCA can be run on any topology of bounded degree (such as pipelines, rings, or ranked trees), and communication may take place between any two processes that are adjacent in the topology. Parameterized verification asks if there is a topology from a given topology class that allows for an accepting run of the given PCA. In general, this problem is undecidable even for synchronous communication and simple pipeline topologies. We therefore consider context-bounded verification, which restricts the behavior of each single process. For several variants of context bounds, we show that parameterized verification over pipelines, rings, and ranked trees is decidable. More precisely, it is PSPACE-complete for pipelines and rings, and EXPTIME-complete for ranked trees. Our approach is automata-theoretic and uniform. We introduce a notion of graph acceptor that identifies those topologies allowing for an accepting run. Depending on the given topology class, the topology acceptor can then be restricted, or adjusted, so that the verification problem reduces to checking emptiness of finite automata or tree automata.

  • Arnaud Sangnier, Parameterized Verification of Broadcast Networks [abstract] [Slides]

    We study decision problems for parameterized verification of a formal model of networks with broadcast communication in which the number of participants as the communication topoloby are paramters. The configuration of such a model can be represented thanks to graphs where nodes are labelled with states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via broadcast messages. Reception of a broadcast is restricted to single-hop neighbors.

    For this model we first consider qualitative verification problems that can be expressed as reachability of configurations with one node (resp. all nodes) in a certain state from an initial configuration with an arbitrary number of nodes and unknown topology. We show that when the topology remains unchanged during an execution, even these basic problems are undecidable but that adding non-deterministic reconfiguration of the communication topology allows to regain decidability. Furthermore when dealing with reconfiguration we propose efficient algorithms to solve reachability queries with cardinality constraints which can express properties on the number of nodes present in the reached graphs. Finally, we prove that we can add probabilistic internal choices to the model with reconfiguration without losing decidability.

Ajouter un attachement

Seuls les utilisateurs autorisés peuvent publier de nouveaux attachements.
« Cette page (révision-67) a été modifiée pour la dernière fois le 24-juin-2014 11:49 par cortier