Automata for modeling real-time systems, ICALP, p.322335, 1990. ,
DOI : 10.1007/BFb0032042
The theory of timed automata, REX Workshop, p.4573, 1991. ,
Causes of the 2003 Major Grid Blackouts in North America and Europe, and Recommended Means to Improve System Dynamic Performance, IEEE Transactions on Power Systems, vol.20, issue.4, 2004. ,
DOI : 10.1109/TPWRS.2005.857942
Principles of model checking, 2008. ,
Coupling and Importance Sampling for Statistical Model Checking, TACAS'12, 2012. ,
DOI : 10.1007/978-3-642-28756-5_23
URL : https://hal.archives-ouvertes.fr/hal-00776795
Statistical abstraction and model-checking of large heterogeneous systems, LNCS, vol.6117, p.3246, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-01055148
Verication of an AFDX infrastructure using simulations and probabilities, Proceedings of the First international conference on Runtime verication, RV'10, p.330344, 2010. ,
Incremental componentbased construction and verication of a robotic system, ECAI, 2008. ,
Modeling Heterogeneous Real-time Systems in BIP, SEFM06, p.312, 2006. ,
URL : https://hal.archives-ouvertes.fr/tel-00527491
Monitoring of realtime properties, FSTTCS, p.260272, 2006. ,
An inequality and associated maximization technique in statistical estimation for probabilistic functions of Markov processes, Inequalities, vol.3, p.18, 1972. ,
An inequality with applications to statistical estimation for probabilistic functions of Markov processes and to a model for ecology, Bulletin of the American Mathematical Society, vol.73, issue.3, p.360, 1967. ,
Statistical inference for probabilistic functions of nite state Markov chains, The Annals of Mathematical Statistics, vol.37, issue.6, p.15541563, 1966. ,
A Maximization Technique Occurring in the Statistical Analysis of Probabilistic Functions of Markov Chains, The Annals of Mathematical Statistics, vol.41, issue.1, p.164171, 1970. ,
DOI : 10.1214/aoms/1177697196
Growth transformations for functions on manifolds, Pacic Journal of Mathematics, vol.27, issue.2, p.211227, 1968. ,
Minimum-Cost Reachability for Priced Timed Automata, HSCC, p.147161, 2001. ,
DOI : 10.7146/brics.v8i3.20457
Axel Legay, and journal = Software Tools for Technology Transfer year =, 2014. ,
A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems, SC'11, 2011. ,
DOI : 10.1002/rob.20206
Statistical model checking: Present and future, RV, 2010. ,
Ayoub Nouri, and Doron Peled. Synthesizing distributed scheduling implementation for probabilistic component-based systems Maximum likelihood alignment of dna sequences, MEMOCODE, 1986. ,
The Algebra of Connectors—Structuring Interaction in BIP, IEEE Transactions on Computers, vol.57, issue.10, p.13151330, 2008. ,
DOI : 10.1109/TC.2008.26
Arnd Hartmanns, and Holger Hermanns . Partial order methods for statistical model checking and simulation, 2011. ,
distributable statistical model checking library, Quantitative Evaluation of Systems, p.160164, 2013. ,
Model-Based Testing of Reactive Systems, Advanced Lectures [The volume is the outcome of a research seminar that was held in Schloss Dagstuhl, Lecture Notes in Computer Science, vol.3472, 2004. ,
Sequential Monte Carlo for rare event estimation, Statistics and Computing, vol.22, p.795808, 2012. ,
Estimating the probability of false alarm for a zero-bit watermarking technique ,
Adaptive multilevel splitting for rare event analysis. Stochastic Analysis and Applications, p.417443, 2007. ,
Finding rare numerical stability errors in concurrent computations, Proceedings of the 2013 International Symposium on Software Testing and Analysis, ISSTA 2013, p.1222, 2013. ,
DOI : 10.1145/2483760.2483791
Crossentropy based testing, FMCAD, p.101108, 2007. ,
Using cross-entropy for satisability, SAC, pp.1196-1203, 2013. ,
The algebraic theory of context-free languages, Studies in Logic and the Foundations of Mathematics, p.118161, 1963. ,
Design and synthesis of synchronization skeletons using branching-time temporal logic, Logic of Programs, p.5271, 1981. ,
Statistical model checking for cyberphysical systems, ATVA, p.112, 2011. ,
Abstract interpretation: A unied lattice model for static analysis of programs by construction or approximation of xpoints, POPL, p.238252, 1977. ,
Adaptive importance sampling simulation of queueing networks, Winter Simulation Conference, p.646655, 2000. ,
Feynman-Kac Formulae: Genealogical and Interacting Particle Systems with Applications. Probability and Its Applications, 2004. ,
Concentration inequalities for mean eld particle models, The Annals of Applied Probability, vol.21, p.10171052, 2011. ,
Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM, vol.18, issue.8, p.453457, 1975. ,
What is a stochastic process?, American Mathematical Monthly, vol.49, p.648653, 1942. ,
Stochastic process, 1953. ,
Sometimes and Not Never revisited: On branching versus linear time, POPL, p.127140, 1983. ,
Runtime verication of component-based systems, In SEFM, p.204220, 2011. ,
Runtime verication of component-based systems in the BIP framework with formally-proved sound and complete instrumentation, p.127, 2013. ,
Checking nite traces using alternating automata, Form. Methods Syst. Des, vol.24, issue.2, p.101127, 2004. ,
The growth of software testing, Communications of the ACM, vol.31, issue.6, p.31687695, 1988. ,
DOI : 10.1145/62959.62965
Automata-based verication of temporal properties on running programs, Proceedings of the 16th IEEE international conference on Automated software engineering, ASE '01, p.412, 2001. ,
Exact stochastic simulation of coupled chemical reactions, Journal of Physical Chemistry, vol.81, p.23402361, 1977. ,
Partial-Order Methods for the Verication of Concurrent Systems -An Approach to the State-Explosion Problem, Lecture Notes in Computer Science, vol.1032, 1996. ,
Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, p.174186, 1997. ,
DOI : 10.1145/263699.263717
Monte Carlo Model Checking, TACAS, p.271286, 2005. ,
DOI : 10.1007/978-3-540-31980-1_18
Monte Carlo methods, 1964. ,
Termination of probabilistic concurrent program, ACM Trans. Program. Lang. Syst, vol.5, issue.3, p.356380, 1983. ,
Model checking JAVA programs using JAVA PathFinder, International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.4, p.366381, 2000. ,
DOI : 10.1007/s100090050043
Synthesizing Monitors for Safety Properties, TACAS, LNCS, p.342356, 2002. ,
DOI : 10.1007/3-540-46002-0_24
Fast simulation of rare events in queueing and reliability models, ACM Transactions on Modeling and Computer Simulation, vol.5, issue.1, p.4385, 1995. ,
DOI : 10.1145/203091.203094
The theory of hybrid automata, LICS ,
Software verication with BLAST, SPIN, p.235239, 2003. ,
DOI : 10.1007/3-540-44829-2_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.6477
Frédéric Magniette, and Sylvain Peyronnet Approximate Probabilistic Model Checking, VMCAI, p.7384, 2004. ,
Probability inequalities, Journal of the American Statistical Association, vol.58, p.1330, 1963. ,
Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association, vol.58, issue.301, p.1330, 1963. ,
SPIN model checking: an introduction, International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.4, p.321327, 2000. ,
DOI : 10.1007/s100090050039
A Study on the Cross-Entropy Method for Rare-Event Probability Estimation, INFORMS Journal on Computing, vol.19, issue.3, p.381394, 2007. ,
DOI : 10.1287/ijoc.1060.0176
Software monitoring with controllable overhead, International Journal on Software Tools for Technology Transfer, vol.38, issue.2, p.327347, 2012. ,
DOI : 10.1007/s10009-010-0184-4
The economic impacts of inadequate infrastructure for software testing, 2002. ,
How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison, HVC ,
DOI : 10.1007/978-3-540-77966-7_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.81.7564
Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking, CAV, 2012. ,
DOI : 10.1007/978-3-642-31424-7_26
URL : https://hal.archives-ouvertes.fr/hal-01087341
A Platform for High Performance Statistical Model Checking ??? PLASMA, TACAS, p.498503, 2012. ,
DOI : 10.1007/978-3-642-28756-5_37
URL : https://hal.archives-ouvertes.fr/hal-01087824
Importance Splitting for Statistical Model Checking Rare Properties, CAV, p.576591, 2013. ,
DOI : 10.1007/978-3-642-39799-8_38
An eective heuristic for adaptive importance splitting in statistical model checking, ISoLA, 2014. ,
Marko chains as an aid in the study of Marko processes, Scandinavian Actuarial Journal, p.8791, 1953. ,
Fast Simulation of Markov Chains with Small Transition Probabilities, Management Science, vol.47, issue.4, p.547562, 2001. ,
DOI : 10.1287/mnsc.47.4.547.9827
Monte Carlo) Attenuation Analysis, 1949. ,
Estimation of Particle Transmission by Random Sampling, In Applied Mathematics, vol.5, 1951. ,
Methods of Reducing Sample Size in Monte Carlo Computations, Journal of the Operations Research Society of America, vol.1, issue.5, 1953. ,
DOI : 10.1287/opre.1.5.263
Runtime verication with particle ltering, RV, p.149166, 2013. ,
DOI : 10.1007/978-3-642-40787-1_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.361.2568
Model checking as control: Feedback control for statistical model checking of cyber-physical systems, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01087977
Simulation-Based CTMC Model Checking: An Empirical Evaluation, 2009 Sixth International Conference on the Quantitative Evaluation of Systems, p.3140, 2009. ,
DOI : 10.1109/QEST.2009.25
The ins and outs of the probabilistic model checker MRMC ,
Grundbegrie der Wahrscheinlichkeitsrechnung, 1933. ,
Statistical characteristics and multiplexing of MPEG streams, Proceedings of INFOCOM'95, p.455462, 1995. ,
DOI : 10.1109/INFCOM.1995.515909
On the characterization of VBR MPEG streams, SIGMETRICS, p.192202, 1997. ,
Information Theory and Statistics, 1968. ,
PRISM: Probabilistic Symbolic Model Checker, Computer Performance Evaluation / TOOLS, p.200204, 2002. ,
DOI : 10.1007/3-540-46029-2_13
PRISM 2.0: a tool for probabilistic model checking, First International Conference on the Quantitative Evaluation of Systems, 2004. QEST 2004. Proceedings., p.322323, 2004. ,
DOI : 10.1109/QEST.2004.1348048
RARE EVENT SIMULATION, Probability in the Engineering and Informational Sciences, p.4566, 2006. ,
DOI : 10.1214/aoap/1034968137
URL : https://hal.archives-ouvertes.fr/hal-00644139
Frédéric Magniez, Sylvain Peyronnet, and Michel de Rougemont Probabilistic abstraction for model checking: An approach based on property testing, ACM TCS, vol.8, issue.4, 2007. ,
Verication of timed and hybrid systems, In ICATPN, p.3942, 2000. ,
Uppaal in a nutshell, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, p.134152, 1997. ,
DOI : 10.1007/s100090050010
Statistical model checking : An overview. CoRR, abs, 1005. ,
DOI : 10.1007/978-3-642-16612-9_11
URL : https://hal.archives-ouvertes.fr/inria-00591593
Scalable verication of Markov decision processes, 4th Workshop on Formal Methods in the Development of Software (FMDS 2014), 2014. ,
On the Advantage of Free Choice: A Symmetric and Fully Distributed Solution to the Dining Philosophers Problem (Extended Abstract), Proc. 8th Ann. Symposium on Principles of Programming Languages, p.133138, 1981. ,
Investigation of the therac-25 accidents, IEEE Computer, vol.26, issue.7, p.1841, 1993. ,
Ariane 501 inquiry board report, 1996. ,
Symbolic model checking, Kluwer, 1993. ,
The Monte Carlo Method, Journal of the American Statistical Association, vol.44, issue.247, p.335341, 1949. ,
DOI : 10.1080/01621459.1949.10483310
Sur une généralisation des intégrales de m.j. radon, Fundamenta Mathematicae, vol.15, p.131179, 1930. ,
SBIP: A statistical model checking extension for the BIP framework, First Workshop on Statistical Model Checking, 2013. ,
Some inequalities relating to the partial sum of binomial probabilities, Annals of the Institute of Statistical Mathematics, vol.7, issue.1, p.2935, 1959. ,
DOI : 10.1007/BF02883985
Stochastic Processes, 1962. ,
DOI : 10.1137/1.9781611971125
The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), p.4657, 1977. ,
DOI : 10.1109/SFCS.1977.32
Time and Modality, 1957. ,
Statistical model checking using perfect simulation, ATVA, p.120134, 2009. ,
A tutorial on hidden Markov models and selected applications in speech recognition, Proceedings of the IEEE, vol.77, issue.2, p.257286, 1989. ,
Stochastic modeling and performance analysis of multimedia socs, ICSAMOS, p.145154, 2013. ,
Rare Event Simulation for Highly Dependable Systems with Fast Repairs, 2010 Seventh International Conference on the Quantitative Evaluation of Systems, pp.69336-355, 2012. ,
DOI : 10.1109/QEST.2010.39
Rare Event Simulation for Highly Dependable Systems with Fast Repairs, 2010 Seventh International Conference on the Quantitative Evaluation of Systems, p.336355, 2012. ,
DOI : 10.1109/QEST.2010.39
Temporal Logic, 1971. ,
DOI : 10.1007/978-3-7091-7664-1
Importance Sampling Simulations of Markovian Reliability Systems Using Cross-Entropy, Annals of Operations Research, vol.40, issue.7, p.119136, 2005. ,
DOI : 10.1007/s10479-005-5727-9
Asymptotic optimality of the cross-entropy method for Markov chain problems, Procedia Computer Science, vol.1, issue.1, pp.1571-1578, 2010. ,
DOI : 10.1016/j.procs.2010.04.176
Monte Carlo statistical methods, 2004. ,
Allen linear (interval) temporal logic translation to LTL and monitor synthesis, CAV, p.263277, 2006. ,
Rare Event Simulation using Monte Carlo Methods, 2009. ,
DOI : 10.1002/9780470745403
URL : https://hal.archives-ouvertes.fr/hal-00787654
The Cross-Entropy Method for Combinatorial and Continuous Optimization, p.127190, 1999. ,
Statistical Model Checking of Black-Box Probabilistic Systems, CAV, p.202215 ,
DOI : 10.1007/978-3-540-27813-9_16
On Statistical Model Checking of Stochastic Systems, CAV, p.266280, 2005. ,
DOI : 10.1007/11513988_26
VESTA: A statistical model-checker and analyzer for probabilistic systems, Second International Conference on the Quantitative Evaluation of Systems (QEST'05), pp.251-252, 2005. ,
DOI : 10.1109/QEST.2005.42
Importance Sampling for the Simulation of Highly Reliable Markovian Systems, Management Science, vol.40, issue.3, p.333352, 1994. ,
DOI : 10.1287/mnsc.40.3.333
Axiomatic derivation of the principle of maximum entropy and the principle of minimum cross-entropy, IEEE Transactions on Information Theory, vol.26, issue.1, p.2637, 1980. ,
A unied approach for studying the properties of transition systems, Theor. Comput. Sci, vol.18, p.227258, 1982. ,
Conditional Markov processes. Theory of Probability and its Applications, p.156178, 1960. ,
Automatic verication of probabilistic concurrent nite-state programs, FOCS, p.327338, 1985. ,
Alternating automata and program verication, Computer Science Today, p.471485, 1995. ,
DOI : 10.1007/bfb0015261
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.2048
RESTART: A Method for Accelerating Rare Event Simulations, Queueing, Performance and Control in ATM, p.7176, 1991. ,
RESTART: a straightforward method for fast simulation of rare events, Proceedings of Winter Simulation Conference, p.282289, 1994. ,
DOI : 10.1109/WSC.1994.717150
Sequential tests of statistical hypotheses, Annals of Mathematical Statistics, vol.16, issue.2, p.117186, 1945. ,
Quality of service (QoS) metrics for continuous media, Multimedia Tools and Applications, vol.3, issue.No. 1, p.127166, 1996. ,
DOI : 10.1007/BF00429748
Lectures on formal methods and performance analysis. chapter Constructing automata from temporal logic formulas: a tutorial, pp.261-277, 2002. ,
Probabilistic verication for "black-box" systems, CAV, p.253265, 2005. ,
Verication and Planning for Stochastic Processes with Asynchronous Events, 2005. ,
Statistical verication of probabilistic properties with unbounded until, SBMF, p.144160, 2010. ,
Statistical probabilistic model checking with a focus on time-bounded properties, Inf. Comput, vol.204, issue.9, pp.1368-1409, 2006. ,
YMER: A Statistical Model Checker, LNCS, vol.3576, p.171179 ,
Probabilistic verication of discrete event systems using acceptance sampling, CAV, p.2339 ,
Logic and Model Checking for Hidden Markov Models, p.98112, 2005. ,
DOI : 10.1109/83.199925
Rare-event verication for stochastic hybrid systems, In HSCC, p.217226, 2012. ,
Bayesian statistical model checking with application to Stateow/Simulink verication. Formal Methods in System Design, p.338367, 2013. ,