{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T05:24:05Z","timestamp":1738992245072,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540926863"},{"type":"electronic","value":"9783540926870"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-92687-0_4","type":"book-chapter","created":{"date-parts":[[2009,2,10]],"date-time":"2009-02-10T09:25:38Z","timestamp":1234257938000},"page":"46-60","source":"Crossref","is-referenced-by-count":3,"title":["Temporalization of Probabilistic Propositional Logic"],"prefix":"10.1007","author":[{"given":"Pedro","family":"Baltazar","sequence":"first","affiliation":[]},{"given":"Paulo","family":"Mateus","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Automata, Languages and Programming","author":"C. Baier","year":"1997","unstructured":"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.\u00a01256, pp. 430\u2013440. Springer, Heidelberg (1997)"},{"key":"4_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-05355-3","volume-title":"Algorithms in Real Algebraic Geometry","author":"S. Basu","year":"2003","unstructured":"Basu, S., Pollack, R., Marie-Fran\u00e7oise, R.: Algorithms in Real Algebraic Geometry. Springer, Heidelberg (2003)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Brinkmann, R., Drechsler, R.: RTL-datapath verification using integer linear programming. In: VLSI Design, pp. 741\u2013746 (2002)","DOI":"10.1109\/ASPDAC.2002.995022"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1145\/62212.62257","volume-title":"STOC 1988: Proceedings of the twentieth annual ACM symposium on Theory of computing","author":"J. Canny","year":"1988","unstructured":"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\u2013469. ACM, New York (1988)"},{"issue":"1-2","key":"4_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.tcs.2007.02.040","volume":"379","author":"R. Chadha","year":"2007","unstructured":"Chadha, R., Cruz-Filipe, L., Mateus, P., Sernadas, A.: Reasoning about probabilistic sequential programs. Theoretical Computer Science\u00a0379(1-2), 142\u2013165 (2007)","journal-title":"Theoretical Computer Science"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2005","unstructured":"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.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-24605-3_7","volume-title":"Theory and Applications of Satisfiability Testing","author":"E.M. Clarke","year":"2004","unstructured":"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.\u00a02919, pp. 78\u201392. Springer, Heidelberg (2004)"},{"issue":"1\/2","key":"4_CR8","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1016\/0890-5401(90)90060-U","volume":"87","author":"R. Fagin","year":"1990","unstructured":"Fagin, R., Halpern, J.Y., Megiddo, N.: A logic for reasoning about probabilities. Information and Computation\u00a087(1\/2), 78\u2013128 (1990)","journal-title":"Information and Computation"},{"key":"4_CR9","first-page":"163","volume-title":"Proceedings 7th Symp. on Principles of Programming Languages, POPL 1980","author":"D. Gabbay","year":"1980","unstructured":"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\u2013173. ACM, New York (1980)"},{"key":"4_CR10","unstructured":"Jones, C.: Probabilistic Non-Determinism. PhD thesis, U. Edinburgh (1990)"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D. Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. Journal of Computer System Science\u00a030, 162\u2013178 (1985)","journal-title":"Journal of Computer System Science"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S.A. Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic. I. Normal modal propositional calculi. Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik\u00a09, 67\u201396 (1963)","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"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.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"issue":"4","key":"4_CR14","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/1059816.1059820","volume":"32","author":"M. Kwiatkowska","year":"2005","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking in practice: case studies with PRISM. SIGMETRICS Perform. Eval. Rev.\u00a032(4), 16\u201321 (2005)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"issue":"5","key":"4_CR15","doi-asserted-by":"publisher","first-page":"771","DOI":"10.1016\/j.ic.2006.02.001","volume":"204","author":"P. Mateus","year":"2006","unstructured":"Mateus, P., Sernadas, A.: Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation\u00a0204(5), 771\u2013794 (2006)","journal-title":"Information and Computation"},{"key":"4_CR16","unstructured":"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.\u00a01, pp. 165\u2013194 (2005)"},{"issue":"3","key":"4_CR17","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C. Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems\u00a018(3), 325\u2013353 (1996)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"4_CR18","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-92687-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,7]],"date-time":"2025-02-07T15:25:27Z","timestamp":1738941927000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-92687-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540926863","9783540926870"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-92687-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}