In: Kroening, D., Pasareanu, C.S., (eds.) Proceedings of 27th International Conference on Computer Aided Verification (CAV 2015), Lecture Notes in Computer Science, vol. Springer, Cham (2016)ĭe Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s () is broken: The good, the bad and the worst case. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. Wiley, Hoboken (2005)Īhrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. Puterman, M.L.: Markov Decision Processes. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Foundations of Computing, MIT Press, Cambridge (2000) Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Springer, Cham (2005)ĭijkstra, E.W.: A discipline of programming. McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems. ACM (2017)īatz, K., et al.: Foundations for entailment checking in quantitative separation logic. In: Castagna, G., Gordon, A.D., (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), pp. Smolka, S., Kumar, P., Foster, N., Kozen, D., Silva, A.: Cantor meets Scott: semantic foundations for probabilistic networks. In: Proceedings on 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021), pp. Stein, D., Staton, S.: Compositional semantics for probabilistic programs with exact conditioning. PhD thesis, RWTH Aachen University, Germany (2019) Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. In: Proceedings of ACM Programming Language, 4(POPL), pp. Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: induction for lower bounds in probabilistic program verification. In: Proceedings 20th Annual Symposium on Foundations of Computer Science, IEEE Computer Society, 101–114 (1979) Kozen, D.: Semantics of probabilistic programs. Finally, we demonstrate the use of pDL to reason about program behavior. We study basic properties of pDL, such as weakening and distribution, that can support reasoning systems. The satisfaction relation is modeled after PCTL, but extended from propositional to first-order setting of dynamic logic, and also embedding program fragments. Since pDL embeds pGCL programs in its box-modality operator, pDL satisfiability builds on a formal MDP semantics for pGCL programs. In order to precisely explain the meaning of specifications, we formally define the satisfaction relation for pDL. The proposed logic pDL can express both first-order state properties and probabilistic reachability properties, addressing both the non-deterministic and probabilistic choice operators of pGCL. This paper introduces the probabilistic dynamic logic pDL, a specification logic for programs in the probabilistic guarded command language ( pGCL) of McIver and Morgan. The semantics of probabilistic languages has been extensively studied, but specification languages for their properties have received little attention.
0 Comments
Leave a Reply. |
Details
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |