Skip to main content
SpringerLink
Log in

Temporalization of Probabilistic Propositional Logic

  • Conference paper
Logical Foundations of Computer Science (LFCS 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5407))

Included in the following conference series:

Abstract

In this paper we study several properties of the Exogenous Probabilistic Propositional Logic (EPPL ), a logic for reasoning about probabilities, with the purpose of introducing a temporal version - Exogenous Probabilistic Linear Temporal Logic (EPLTL). In detail, we give a small model theorem for EPPL and introduce a satisfaction and a model checking algorithm for both EPPL and EPLTL. We are also able to provide a (weakly) complete calculus for EPLTL. Finally, we conclude by pointing out some future work.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baier, C., Clarke, E., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 430–440. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  2. Basu, S., Pollack, R., Marie-Françoise, R.: Algorithms in Real Algebraic Geometry. Springer, Heidelberg (2003)

    Book  MATH  Google Scholar 

  3. Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: VLSI Design, pp. 741–746 (2002)

    Google Scholar 

  4. Canny, J.: Some algebraic and geometric computations in pspace. In: STOC 1988: Proceedings of the twentieth annual ACM symposium on Theory of computing, pp. 460–469. ACM, New York (1988)

    Chapter  Google Scholar 

  5. Chadha, R., Cruz-Filipe, L., Mateus, P., Sernadas, A.: Reasoning about probabilistic sequential programs. Theoretical Computer Science 379(1-2), 142–165 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  6. Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Clarke, E.M., Talupur, M., Veith, H., Wang, D.: Sat based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 78–92. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Fagin, R., Halpern, J.Y., Megiddo, N.: A logic for reasoning about probabilities. Information and Computation 87(1/2), 78–128 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  9. Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: The temporal analysis of fairness. In: Proceedings 7th Symp. on Principles of Programming Languages, POPL 1980, pp. 163–173. ACM, New York (1980)

    Google Scholar 

  10. Jones, C.: Probabilistic Non-Determinism. PhD thesis, U. Edinburgh (1990)

    Google Scholar 

  11. Kozen, D.: A probabilistic PDL. Journal of Computer System Science 30, 162–178 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  12. Kripke, S.A.: Semantical analysis of modal logic. I. Normal modal propositional calculi. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 9, 67–96 (1963)

    Article  MathSciNet  MATH  Google Scholar 

  13. Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)

    Google Scholar 

  14. Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking in practice: case studies with PRISM. SIGMETRICS Perform. Eval. Rev. 32(4), 16–21 (2005)

    Article  Google Scholar 

  15. Mateus, P., Sernadas, A.: Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation 204(5), 771–794 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  16. Mateus, P., Sernadas, A., Sernadas, C.: Exogenous semantics approach to enriching logics. In: Sica, G. (ed.) Essays on the Foundations of Mathematics and Logic, Polimetrica, vol. 1, pp. 165–194 (2005)

    Google Scholar 

  17. Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)

    Article  Google Scholar 

  18. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. SQIG-Instituto de Telecomunicações and IST, Portugal

    Pedro Baltazar & Paulo Mateus

Authors
  1. Pedro Baltazar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paulo Mateus
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science, CUNY Graduate Center, 365 Fifth Avenue, NY 10016, New York, USA

    Sergei Artemov

  2. Department of Mathematics, Cornell University, 545 Malott Hall, NY 14853, Ithaca, USA

    Anil Nerode

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baltazar, P., Mateus, P. (2008). Temporalization of Probabilistic Propositional Logic. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2009. Lecture Notes in Computer Science, vol 5407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92687-0_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-92687-0_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-92686-3

  • Online ISBN: 978-3-540-92687-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation