Abstract
The aims of these lecture notes are two-fold: (i) we investigate the relation between the operational semantics of probabilistic programming languages and Discrete Time Markov Chains (DTMCs), and (ii) we present a framework for probabilistic program analysis which is inspired by the classical Abstract Interpretation framework by Cousot & Cousot and which we introduced as Probabilistic Abstract Interpretation (PAI) in [1]. The link between programming languages and DTMCs is the construction of a so-called Linear Operator semantics (LOS) in a syntax-directed or compositional way. The main element in this construction is the use of tensor product to combine information about different aspects of a program. Although this inevitably results in a combinatorial explosion of the size of the semantics of program, the PAI approach allows us to keep some control and to obtain reasonably sized abstract models.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Di Pierro, A., Wiklicky, H.: Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation. In: PPDP 2000, pp. 127–138 (2000)
Di Pierro, A., Hankin, C., Wiklicky, H.: Continuous-time probabilistic KLAIM. In: Focardi, R., Zavattaro, G. (eds.) SecCo 2004 — CONCUR Workshop on Security Issues in Coordination Models, Languages and Systems. ENTCS, vol. 128(5). Elsevier, Amsterdam (2005)
Stirzaker, D.: Probability and Random Variables – A Beginners Guide. Cambridge University Press, Cambridge (1999)
Greub, W.: Linear Algebra. In: Grundlehren der mathematischen Wissenschaften, 3rd edn., vol. 97. Springer, New York (1967)
Conway, J.: A Course in Functional Analysis. In: Garduate Texts in Mathematics, 2nd edn., vol. 96. Springer, New York (1990)
Seneta, E.: Non-negative Matrices and Markov Chains, 2nd edn. Springer, Heidelberg (1981)
Grimmett, G., Stirzaker, D.: Probability and Random Processes, 2nd edn. Clarendon Press, Oxford (1992)
Tijms, H.: Stochastic Models – An Algorithmic Approach. John Wiley & Sons, Chichester (1994)
Grinstead, C., Snell, J.: Introduction to Probability, 2 revised edn. American Mathematical Society, Providence (1997)
Norris, J.: Markov Chains. Cambidge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (1997)
Roman, S.: Advanced Linear Algebra, 2nd edn. Springer, Heidelberg (2005)
Kadison, R., Ringrose, J.: Fundamentals of the Theory of Operator Algebras: Volume I – Elementary Theory. Graduate Studies in Mathematics, vol. 15. American Mathematical Society, Providence (1997); Reprint from Academic Press edition (1983)
Filter, W., Weber, K.: Integration Theory. Chapman and Hall, Boca Raton (1997)
Nielson, F., Nielson, H.R.: Flow logics and operational semantics. ENTCS 10 (1998)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
Di Pierro, A., Hankin, C., Wiklicky, H.: Measuring the confinement of probabilistic systems. Theoretical Computer Science 340(1), 3–56 (2005)
Cousot, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interpretation. In: POPL 2002, pp. 178–190 (2002)
Di Pierro, A., Hankin, C., Wiklicky, H.: A systematic approach to probabilistic pointer analysis. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 335–350. Springer, Heidelberg (2007)
Cousot, P., Cousot, R.: Abstract Interpretation and Applications to Logic Programs. Journal of Logic Programming 13(2-3), 103–180 (1992)
Abramsky, S., Hankin, C. (eds.): Abstract Interpretation of Declarative Languages. Ellis-Horwood, Chichester (1987)
Davey, B., Priestley, H.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)
Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: POPL 1977, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks. In: Proceedings of POPL 1979, San Antonio, Texas, pp. 269–282 (1979)
Di Pierro, A., Hankin, C., Wiklicky, H.: Abstract interpretation for worst and average case analysis. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol. 4444, pp. 160–174. Springer, Heidelberg (2007)
Di Pierro, A., Wiklicky, H.: Measuring the precision of abstract interpretations. In: Lau, K.-K. (ed.) LOPSTR 2000. LNCS, vol. 2042, pp. 147–164. Springer, Heidelberg (2001)
Campbell, S., Meyer, D.: Generalized Inverse of Linear Transformations. Constable and Company, London (1979)
Ben-Israel, A., Greville, T.: Generalised Inverses, 2nd edn. Springer, Heidelberg (2003)
Eaton, J.: Gnu Octave Manual (2002), http://www.octave.org
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Di Pierro, A., Hankin, C., Wiklicky, H. (2010). Probabilistic Semantics and Program Analysis. In: Aldini, A., Bernardo, M., Di Pierro, A., Wiklicky, H. (eds) Formal Methods for Quantitative Aspects of Programming Languages. SFM 2010. Lecture Notes in Computer Science, vol 6154. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13678-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-13678-8_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13677-1
Online ISBN: 978-3-642-13678-8
eBook Packages: Computer ScienceComputer Science (R0)