Paulevé, L. ; Andrieux, G. ; Koeppl, H. (2013)
Under-approximating cut sets for reachability in large scale automata Networks.
25th International Conference on Computer Aided Verification (CAV 2013).
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
In the scope of discrete finite-state models of interacting components, we present a novel algorithm for identifying sets of local states of components whose activity is necessary for the reachability of a given local state. If all the local states from such a set are disabled in the model, the concerned reachability is impossible.</br>Those sets are referred to as cut sets and are computed from a particular abstract causality structure, so-called Graph of Local Causality, inspired from previous work and generalised here to finite automata networks. The extracted sets of local states form an under-approximation of the complete minimal cut sets of the dynamics: there may exist smaller or additional cut sets for the given reachability.</br>Applied to qualitative models of biological systems, such cut sets provide potential therapeutic targets that are proven to prevent molecules of interest to become active, up to the correctness of the model. Our new method makes tractable the formal analysis of very large scale networks, as illustrated by the computation of cut sets within a Boolean model of biological pathways interactions gathering more than 9000 components.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2013 |
| Autor(en): | Paulevé, L. ; Andrieux, G. ; Koeppl, H. |
| Art des Eintrags: | Bibliographie |
| Titel: | Under-approximating cut sets for reachability in large scale automata Networks |
| Sprache: | Englisch |
| Publikationsjahr: | 2013 |
| Verlag: | Springer |
| Band einer Reihe: | 8044 |
| Veranstaltungstitel: | 25th International Conference on Computer Aided Verification (CAV 2013) |
| URL / URN: | http://link.springer.com/chapter/10.1007%2F978-3-642-39799-8... |
| Kurzbeschreibung (Abstract): | In the scope of discrete finite-state models of interacting components, we present a novel algorithm for identifying sets of local states of components whose activity is necessary for the reachability of a given local state. If all the local states from such a set are disabled in the model, the concerned reachability is impossible.</br>Those sets are referred to as cut sets and are computed from a particular abstract causality structure, so-called Graph of Local Causality, inspired from previous work and generalised here to finite automata networks. The extracted sets of local states form an under-approximation of the complete minimal cut sets of the dynamics: there may exist smaller or additional cut sets for the given reachability.</br>Applied to qualitative models of biological systems, such cut sets provide potential therapeutic targets that are proven to prevent molecules of interest to become active, up to the correctness of the model. Our new method makes tractable the formal analysis of very large scale networks, as illustrated by the computation of cut sets within a Boolean model of biological pathways interactions gathering more than 9000 components. |
| Fachbereich(e)/-gebiet(e): | 18 Fachbereich Elektrotechnik und Informationstechnik 18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Nachrichtentechnik > Bioinspirierte Kommunikationssysteme 18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Nachrichtentechnik |
| Hinterlegungsdatum: | 04 Apr 2014 12:22 |
| Letzte Änderung: | 23 Sep 2021 14:31 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum