Algebraic decision diagrams and their applications. Formal Methods in System Design, pp.171-206, 1997. ,
DOI : 10.1109/iccad.1993.580054
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.2128
Model checking of probabilistic and nondeterministic systems, Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95), volume 1026 of LNCS, pp.499-513, 1995. ,
DOI : 10.1007/3-540-60692-0_70
An algorithm for strongly connected component analysis in n log n symbolic steps, Proc. 3rd International Conference on Formal Methods in Computer- Aided Design (FMCAD'00), pp.37-54, 2000. ,
Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.35677-691, 1986. ,
DOI : 10.1109/TC.1986.1676819
Self-adaptive software needs quantitative verification at runtime, Communications of the ACM, vol.55, issue.9, 2012. ,
DOI : 10.1145/2330667.2330686
Dynamic QoS Management and Optimization in Service-Based Systems, IEEE Transactions on Software Engineering, vol.37, issue.3, pp.387-409, 2011. ,
DOI : 10.1109/TSE.2010.92
Reduction Techniques for Model Checking Markov Decision Processes, 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp.45-54, 2008. ,
DOI : 10.1109/QEST.2008.45
Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design, pp.10149-169, 1997. ,
Incremental algorithms for interprocedural analysis of safety properties, Proc. CAV'05, pp.449-461, 2005. ,
The complexity of probabilistic verification, Journal of the ACM, vol.42, issue.4, pp.857-907, 1995. ,
DOI : 10.1145/210332.210339
Symbolic and Parametric Model Checking of Discrete-Time Markov Chains, Proc. 1st Int Coll. Theoretical Aspects of Computing, pp.280-294, 2004. ,
DOI : 10.1007/978-3-540-31862-0_21
Formal Verification of Probabilistic Systems, 1997. ,
Automated Learning of Probabilistic Assumptions for Compositional Reasoning, Proc. 14th International Conference on Fundamental Approaches to Software Engineering (FASE'11), pp.2-17, 2011. ,
DOI : 10.1007/978-3-642-19811-3_2
URL : https://hal.archives-ouvertes.fr/hal-00647067
Self-adaptive software meets control theory: A preliminary approach supporting reliability requirements, 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), pp.283-292, 2011. ,
DOI : 10.1109/ASE.2011.6100064
Run-time efficient probabilistic model checking, Proceeding of the 33rd international conference on Software engineering, ICSE '11, 2011. ,
DOI : 10.1145/1985793.1985840
Automated Verification Techniques for Probabilistic Systems, Formal Methods for Eternal Networked Software Systems (SFM'11), pp.53-113, 2011. ,
DOI : 10.1007/978-3-642-21455-4_3
URL : https://hal.archives-ouvertes.fr/hal-00648037
Computing strongly connected components in a linear number of symbolic steps, Proc. SODA'03, pp.573-582, 2003. ,
Synthesis for PCTL in Parametric Markov Decision Processes, Proc. 3rd NASA Formal Methods Symposium (NFM'11), 2011. ,
DOI : 10.1214/aoms/1177699369
PARAM: A Model Checker for Parametric Markov Models, Proc. 22nd International Conference on Computer Aided Verification (CAV'10), pp.660-664, 2010. ,
DOI : 10.1007/978-3-642-14295-6_56
URL : https://hal.archives-ouvertes.fr/hal-00650737
Probabilistic reachability for parametric Markov models, Proc. 16th International SPIN Workshop, pp.88-106, 2009. ,
Approximate parameter synthesis for probabilistic timebounded reachability, Proc. IEEE Real-Time Systems Symposium (RTSS 08), pp.173-182 ,
A logic for reasoning about time and reliability, Formal Aspects of Computing, vol.2, issue.1, pp.512-535, 1994. ,
DOI : 10.1007/BF01211866
Incremental and Complete Bounded Model Checking for Full PLTL, CAV 05, pp.98-111, 2005. ,
DOI : 10.1007/11513988_10
Denumerable Markov Chains, 1976. ,
DOI : 10.1007/978-1-4684-9455-6
PRISM 4.0: Verification of Probabilistic Real-Time Systems, Proc. 23rd International Conference on Computer Aided Verification (CAV'11), pp.585-591, 2011. ,
DOI : 10.1007/3-540-45657-0_17
URL : https://hal.archives-ouvertes.fr/hal-00648035
Probabilistic verification of herman's selfstabilisation algorithm. Formal Aspects of Computing, 2012. ,
Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol, Formal Aspects of Computing, vol.14, issue.3, pp.295-318, 2003. ,
DOI : 10.1007/s001650300007
Incremental quantitative verification for Markov decision processes, 2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN), pp.359-370, 2011. ,
DOI : 10.1109/DSN.2011.5958249
URL : https://hal.archives-ouvertes.fr/hal-00647057
The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977. ,
DOI : 10.1109/SFCS.1977.32
Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1994. ,
DOI : 10.1002/9780470316887
Probabilistic analysis of an anonymity system, Journal of Computer Security, vol.12, issue.3-4, pp.355-377, 2004. ,
DOI : 10.3233/JCS-2004-123-403
Incremental model checking in the modal mu-calculus, CAV 94, pp.351-363, 1994. ,
DOI : 10.1007/3-540-58179-0_67
Alea jacta est: Verification of probabilistic, real-time and parametric systems, 2002. ,
Runtime Verification with State Estimation, Proc. 2nd International Conference on Runtime Verification (RV'11), 2011. ,
DOI : 10.1007/978-3-642-29860-8_15
Depth-first search and linear graph algorithms, SIAM Journal on Computing, vol.136, pp.146-160, 1972. ,