
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
YoungMin Kwon, Gul Agha, "Verifying the Evolution of Probability Distributions Governed by a DTMC," IEEE Transactions on Software Engineering, vol. 37, no. 1, pp. 126141, January/February, 2011.  
BibTex  x  
@article{ 10.1109/TSE.2010.80, author = {YoungMin Kwon and Gul Agha}, title = {Verifying the Evolution of Probability Distributions Governed by a DTMC}, journal ={IEEE Transactions on Software Engineering}, volume = {37}, number = {1}, issn = {00985589}, year = {2011}, pages = {126141}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2010.80}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Verifying the Evolution of Probability Distributions Governed by a DTMC IS  1 SN  00985589 SP126 EP141 EPD  126141 A1  YoungMin Kwon, A1  Gul Agha, PY  2011 KW  Probabilistic model checking KW  linear temporal logic KW  Discrete Time Markov Chain KW  pharmacokinetics. VL  37 JA  IEEE Transactions on Software Engineering ER   
[1] iLTLChecker: http://osl.cs.uiuc.edu/~ykwon4/cgiiLTL.html , 2010.
[2] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, "Verifying Continuous Time Markov Chains," Proc. Eighth Int'l Conf. Computer Aided Verification, pp. 269276, 1996.
[3] A. Aziz, V. Singhal, and F. Balarin, "It Usually Works: The Temporal Logic of Stochastic Systems," Proc. Seventh Int'l Conf. Computer Aided Verification, pp. 155165, 1995.
[4] C. Baier, J. Katoen, and H. Hermanns, "Approximate Symbolic Model Checking of ContinuousTime Markov Chains," Proc. 10th Int'l Conf. Concurrency Theory, pp. 146162, 1999.
[5] B.A. Berg, Markov Chain Monte Carlo Simulation and Their Statistical Analysis. World Scientific Publishing Company, 2004.
[6] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, "Symbolic Model Checking Without BDDs," Proc. Fifth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 193207, 1999.
[7] J. Büchi, "On a Decision Method in Restricted Second Order Arithmetic," Proc. Int'l Conf. Logic, Methodology and Philosophy of Science, pp. 111, 1960.
[8] P. Bucholz, "Exact and Ordinary Lumpability in Finite Markov Chains," J. Applied Probability, vol. 31, pp. 5974, 1994.
[9] M. Calder, A. Duguid, S. Gilmore, and J. Hillston, "Stronger Computational Modelling of Signalling Pathways Using Both Continuous and DiscreteState Methods," Computational Methods in Systems Biology, pp. 6377, SpringerVerlag, 2006.
[10] G. Ciardo, R.A. Marie, B. Sericola, and K.S. Trivedi, "Performability Analysis Using SemiMarkov Reward Process," IEEE Trans. Computers, vol. 39, no. 10, pp. 12511264, Oct. 1990.
[11] G. Ciardo and A.S. Miner, "A Data Structure for the Efficient Kronecker Solution of GSPNs," Proc. Int'l Workshop Petri Nets and Performance Models, pp. 2231, 1999.
[12] E. Clarke and E. Emerson, "Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic," Proc. Workshop Logic of Programs, 1981.
[13] E. Clarke, E. Emerson, and A. Sistla, "Automatic Verification of FiniteState Concurrent Systems Using Temporal Logics Specification: A Practical Approach," Proc. 10th Int'l ACM Symp. Principles of Programming Languages, pp. 117126, 1983.
[14] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 2000.
[15] R. Grosu, E. Bartocci, F. Corradini, E. Entcheva, S. Smolka, and A. Wasilewska, "Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes," Hybrid Systems: Computation and Control, pp. 229243, SpringerVerlag, 2008.
[16] H. Hansson and B. Jonsson, "A Logic for Reasoning about Time and Reliability," Formal Aspects of Computing, vol. 6, pp. 512535, 1994.
[17] G.J. Holzmann, "The Model Checker Spin," IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279295, May 1997.
[18] G. Hughes and M. Creswell, Introduction to Modal Logic. Methuen, 1997.
[19] J.G. Kemeny and J.L. Snell, Finite Markov Chains. SpringerVerlag, 1976.
[20] M. Kwiatkowska, G. Norman, and D. Parker, "Prism 2.0: A Tool for Probabilistic Model Checking," Proc. Int'l Conf. Quantitative Evaluation of Systems, pp. 322323, 2004.
[21] Y. Kwon and G. Agha, "Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains," Proc. Int'l Conf. Formal Eng. Methods, pp. 194208, 2004.
[22] Y. Kwon and G. Agha, "iLTLChecker: A Probabilistic Model Checker for Multiple DTMCs," Proc. Int'l Conf. Quantitative Evaluation of Systems, 2005.
[23] Y. Kwon and G. Agha, "Scalable Modeling and Performance Evaluation of Wireless Sensor Networks," Proc. IEEE RealTime and Embedded Technology and Applications Symp., 2006.
[24] Y. Kwon and G. Agha, "A Markov Reward Model for Software Reliability," Proc. Next Generation Software Workshop at the IEEE Int'l Parallel and Distributed Processing Symp., pp. 16, 2007.
[25] Y. Kwon and G. Agha, "LTLC: Linear Temporal Logic for Control," Hybrid Systems: Computation and Control, pp. 316329, SpringerVerlag, 2008.
[26] V.V. Lam, P. Buchholz, and W.H. Sanders, "A Structured PathBased Approach for Computing Transient Rewards for Large CTMCs," Proc. Int'l Conf. Quantitative Evaluation of Systems, pp. 136145, 2004.
[27] O. Lichtenstein and A. Pnueli, "Checking That Finite State Concurrent Programs Satisfy Their Linear Specification," Proc. 12th ACM Symp. Principles of Programming Languages, pp. 97107, 1985.
[28] D.G. Luenberger, Linear and Nonlinear Programming, second ed., Addison Wesley, 1989.
[29] J. Martyna, "Performance Modeling of Mobile Sensor Networks," AdHoc, Mobile, and Wireless Networks, pp. 262272, SpringerVerlag, 2007.
[30] A.S. Miner and G. Ciardo, "Efficient Reachability Set Generation and Storage Using Decision Diagrams," Proc. Int'l Conf. Application and Theory of Petri Nets, pp. 625, 1999.
[31] A. Papoulis, Probability, Random Variables, and Stochastic Processes, third ed. McGrawHill, 1991.
[32] H. Pham, Software Reliability. Springer, 2000.
[33] J. Rajgopal and M. Mazumdar, "Modular Operational Test Plans for Inference on Software Reliability Based on a Markov Model," IEEE Trans. Software Eng., vol. 28, no. 4, pp. 358363, Apr. 2002.
[34] D.M. Roberts and N.A. Buckley, "Pharmacokinetic Considerations in Clinical Toxicology," Clinical Pharmacokinetics, vol. 46, pp. 897939, 2007.
[35] L. Shargel and A.B.C. Yu, Applied Biopharmaceutics and Pharmacokinetics. AppletonCenturyCrofts, 1985.
[36] H. Start and J.W. Woods, Probability and Random Processes with Applications to Signal Processing, third ed., PrenticeHall, 2002.
[37] G. Strang, Linear Algebra and Its Applications, third ed., Harcourt Brace Jova novich, 1988.
[38] A.S. Tanenbaum, Computer Networks, fourth ed., Prentice Hall, 2003.
[39] S.M. Yacoub, B. Cukic, and H.H. Ammar, "ScenarioBased Reliability Analysis of ComponentBased Software," Proc. 10th Int'l Symp. Software Reliability Eng., pp. 2231, 1999.