Pint implements static analyses for computing dynamical properties on very large-scale Automata Networks, ranging from hundreds to several thousands of concurrently interacting components. Provided analyses include notably the listing of fixed points, successive reachability properties, cut sets for reachability, and model reduction preserving transient dynamics. The translation to related formalisms, in particular Boolean and multi-valued networks, is also provided.
Automata Networks are defined by a set of finite-state machines whose local transitions can be conditionned by the state of other automata in the network. Applications are in particlar in systems biology with the modelling and analysis of signalling pathways and gene regulatory networks, gathering multiple interacting components with a few local states.
Pint comes with several command line tools to perform formal analyses, reductions, simulations, and translation to other formalisms. An OCaml library, with possible C bindings, can also be compiled in order to embed the static analyses in other frameworks.
Graphical interfaces for Pint are also available.
- Syntax for Automata Network models (.an)
- Syntax for Process Hitting models (.ph)
- Sufficient conditions for reachability in automata networks with priorities (M. Folschette, L. Paulevé, M. Magnin, and O. Roux in Journal of Theoretical Computer Science, 2015)
- Identification of biological regulatory networks from Process Hitting models (M. Folschette, L. Paulevé, K. Inoue, M. Magnin, and O. Roux in Journal of Theoretical Computer Science, 2015)
- Analyzing Large Network Dynamics with Process Hitting (L. Paulevé, C. Chancellor, M. Folschette, M. Magnin, and O. Roux chapter of Logical Modeling of Biological Systems book.)
- Under-Approximating Cut Sets for Reachability in Large Scale Automata Networks (L. Paulevé, G. Andrieux, H. Koeppl at Computer Aided Verification, 2013)
- Under-approximation of Reachability in Multivalued Asynchronous Networks (M. Folschette, L. Paulevé, M. Magnin, O. Roux at CS2Bio 2013)
- Concretizing the Process Hitting into Biological Regulatory Networks (M. Folschette, L. Paulevé, K. Inoue, M. Magnin, O. Roux at Computational Methods in Systems Biology, 2012)
- Static analysis of biological regulatory networks dynamics using abstract interpretation (L. Paulevé, M. Magnin, O. Roux in Mathematical Structures in Computer Science, 2012)
- Abstract Interpretation of Dynamics of Biological Regulatory Networks (L. Paulevé, M. Magnin, O. Roux at Static Analysis and Systems Biology, 2010)
- Refining Dynamics of Gene Regulatory Networks in a Stochastic π-Calculus (L. Paulevé, M. Magnin, O. Roux in Transactions on Computational Systems Biology, 2011)
Model repository on GitHub.
If you have any question regarding Pint or the Process Hitting, please contact Loïc Paulevé.