logo              Stochastic Models:
Scalable Model Checking. 		                          ANR
Home Members Meetings Tasks Publications Bibliography


  • [AAGT12] M. Agrawal, S. Akshay, B. Genest, and PS Thiagarajan. Approximate verification of the symbolic dynamics of markov chains. LICS'12, 55-64, 2012.
  • [ABSLS08] JG Albeck, JM Burke, SL Spencer, DA Lauffenburger, PK Sorger, Modeling a snap-action, variable-delay switch controlling extrinsic cell death. PLoS Biol. Dec 2;6(12):2831-52, 2008.
  • [BBG08] C. Baier, N. Bertrand, M. Größer: On Decision Problems for Probabilistic Büchi Automata. FoSSaCS'08, p 287-301, 2008.
  • [BK98] X. Boyen and D. Koller. Tractable inference for complex stochastic processes. UAI'98, p 33-42, 1998.
  • [BK08] C. Baier, J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
  • [BKL11] J. Barry, L.Kaelbling, T.Lozano-Pérez: DetH*: Approximate Hierarchical Solution of Large Markov Decision Processes. IJCAI 2011: 1928-1935, 2011.
  • [BG11] N.Bertrand, B.Genest. Minimal Disclosure in Partially Observable Markov Decision Processes. FSTTCS 2011, p. 411-422, 2011.
  • [BHCLSC04] K. S. Brown, C. C. Hill, G. A. Calero, K. H. Lee, J. P. Sethna, and R. A. Cerione. The statistical mechanics of complex signaling networks: nerve growth factor signaling. Physical Biology 1, p/ 184--195, 2004.
  • [BMT77] A. Bertoni, G. Mauri, and M. Torelli. Some recursive unsolvable problems relating to isolated cutpoints in probabilistic automata. ICALP'77, p 87-94, 2007.
  • [BRS02] D. Beauquier, A.Rabinovich, A. Slissenko. A logic of probability with decidable model checking. CSL'02. 306-321, 2002.
  • [BSB12] F. Bertaux, S. Stoma, G. Batt, Stochastic model of TRAIL induced apoptosis explains survival correlations between parental cells, in preparation.
  • [BZ01] D.S. Bernstein and S. Zilberstein. Reinforcement Learning for Weakly-Coupled MDPs and an Application to Planetary Rover Control. ECP'01, 373-378, 2001.
  • [CCKSVW02] P. Chauhan, E. Clarke, J. Kukula, S. Sapra, H. Veith, D. Wang. Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis. FMCAD'02, 2002.
  • [CKVAK11] R.Chadha, V.Korthikanti, M.Viswanathan, G.Agha, Y.Kwon: Model Checking MDPs with a Unique Compact Invariant Set of Distributions. QEST'11: 121-130, 2011.
  • [CT12] K. Chatterjee, M. Tracol. Decidable Problems for Probabilistic Automata on Infinite Words. LICS'12: 185-194, 2012.
  • [DKLLPSW11] B. Delahaye, J.-P. Katoen, K. Larsen, A. Legay, M. Pedersen, F. Sher, A. Wasowski. Abstract Probabilistic Automata. VMCAI'11: 324-339, 2011.
  • [FGO12] N. Fijalkow, H. Gimbert, Y. Oualhad. Deciding the Value 1 Problem for Probabilistic Leaktight Automata. LICS'12: 295-304, 2012.
  • [GH10] Hugo Gimbert, Florian Horn. Solving Simple Stochastic Tail Games. SODA'10: 847-862, 2010.
  • [GO10] Hugo Gimbert, Youssouf Oualhadj. Probabilistic Automata on Finite Words: Decidable and Undecidable Problems. ICALP'10 (2): 527-538, 2010.
  • [HJ94] H. Hansson, B. Jonsson : A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5):512-535, 1994.
  • [HLP06] T.Hérault, R.Lassaigne, S.Peyronnet: APMC 3.0: Approximate Verification of Discrete and Continuous Time Markov Chains. QEST'06: 129-130, 2006.
  • [HHHK05] Vesa Halava , Tero Harju , Mika Hirvensalo , Juhani Karhumäki. Skolem's Problem - On the Border between Decidability and Undecidability. Internal report of Turku, 2005.
  • [KVAK10] V.A. Korthikanti, M. Viswanathan, G. Agha, and Y.M. Kwon. Reasoning about mdps as transformers of probability distributions. QEST'10, p 199--208. 2010.
  • [Kruyt08]F. Kruyt, TRAIL and cancer therapy, Cancer Letters, 263(1), p 14-25, 2008
  • [KS60] J.G. Kemeny and J.L. Snell. Finite markov chains. Springer, 1960.
  • [KZHHJ1] J.-P. Katoen, I. Zapreev, E. Hahn, H. Hermanns, D. Jansen. The ins and outs of the probabilistic model checker MRMC. Performance Evaluation 68(2):90-104, 2011.
  • [LDB10] A.Legay, B.Delahaye, S.Bensalem: Statistical Model Checking: An Overview. RV'10: 122-135, 2010.
  • [LSD11] Y. Liu, J. Sun, J. S.Dong. PAT 3: An Extensible Architecture for Building Multi-domain Model Checkers. ISSRE'11, 190-199, 2011.
  • [LTH11] B. Liu, PS Thiagarajan, and D. Hsu. Probabilistic approximations of odes based bio-pathway dynamics. TCS, 2011.
  • [LLMPR07] S.Laplante, R.Lassaigne, F.Magniez, S.Peyronnet, M.de Rougemont: Probabilistic abstraction for model checking: An approach based on property testing. ACM Trans. Comput. Log. 8(4),2007.
  • [Murphy02] K.P. Murphy. Dynamic bayesian networks: representation, inference and learning. PhD thesis, University of California, 2002.
  • [MW01] K. P. Murphy and Y. Weiss. The factored frontier algorithm for approximate inference in {DBN}s. UAI'01, p 378--385, 2001.
  • [OP12] J. Ouaknine, J.Worrel. Decision problems for linear recurrence sequences. RP'12, LNCS 7550, 2012.
  • [Parr98] R. Parr. Flexible decomposition algorithms for weakly coupled Markov decision problems. UAI'98, 422-430, 1998.
  • [PAGT11] S.K. Palaniappan, S.Akshay, B.Genest, and PSThiagarajan. A hybrid factored frontier algorithm for dynamic bayesian networks. CMSB'11, 35-44, 2011.
  • [PALGT12] S.K. Palaniappan, S.Akshay, B.Liu, B.Genest, and PSThiagarajan. A hybrid factored frontier algorithm for dynamic bayesian networks with a biopathways application. IEEE/ACM Transactions on Computational Biology and Bioinformatics 9(5): 1352-1365, 2012.
  • [Paz71] A. Paz. Introduction to probabilistic automata. Academic Press, Orlando, USA, 1971.
  • [PMR12] L.Paulevé, M.Magnin, O.Roux: Static analysis of Biological Regulatory Networks dynamics using abstract interpretation. Mathematical Structures in Computer Science 22(4): 651-685 (2012).
  • [PRISM11] M. Kwiatkowska, G. Norman, D. Parker. Prism 4.0: Verification of probabilistic real-time systems. CAV'11. LNCS 6806, 585-591, 2011.
  • [Rab63] Michael O. Rabin. Probabilistic automata. Information and Control, 6(3):230-245, 1963.
  • [SDBMB12] S. Stoma,A. Donze, F. Bertaux, O. Maler, G. Batt, STL-based analysis of TRAIL-induced apoptosis challenges the notion of type I/type II cell line classification, INRIA RR-8121; submitted to PLoS Computational Biology, 2012.
  • [SGABS09] SL Spencer, S Gaudet, JG Albeck, JM Burk, PK Sorger. Non-genetic origins of cell-to-cell variability in TRAIL-induced apoptosis. Nature.459(7245):428-32, 2009.
  • [SRMcC07] C.Sutton,A.McCallum,K.Rhanimanesh: Dynamic Conditional Random Fields: Factorized Probabilistic Models for Labeling and Segmenting Sequence Data. Journal of Machine Learning Research 8: 693-723, 2007.
  • [UBFHB11] J. Uhlendorf,S. Bottani,F. Fages, P. Hersen, G. Batt, Towards real-time control of gene expression: controlling the hog signaling cascade, Pac Symp Biocomput. 338-49, 2011.
  • [UMDCFBBH12] Uhlendorf J, Miermont A, Delaveau T, Charvin G, Fages F, Bottani S, Batt G, Hersen P., Long-term model predictive control of gene expression at the population and single-cell levels., Proc Natl Acad Sci U S A. 109(35):14271-6, 2012.
  • [WGMHA10] V. Wolf, R. Goel, M. Mateescu, T. Henzinger. Solving the chemical master equation using sliding windows. BMC Systems Biology 4(42), 2010.
  • [ZRKPPLK12] C. Zechner, J. Ruess, P Krenn, S. Pelet, M. Peter,J. Lygeros, H. Koeppl. Moment-based inference predicts bimodality in transient gene expression., Proc Natl Acad Sci U S A. 109(21):8340-5, 2012