MODEL CHECKING TEMPORAL PROPERTIES OF RECURSIVE PROBABILISTIC PROGRAMS

被引：0

作者：

Winkler, Tobias ^{[1
]}

Gehnen, Christina ^{[1
]}

Katoen, Joost-Pieter ^{[1
]}

机构：

[1] Rhein Westfal TH Aachen, Aachen, Germany

来源：

LOGICAL METHODS IN COMPUTER SCIENCE | 2023年 / 19卷 / 04期

关键词：

Probabilistic Recursive Programs and Model Checking and Probabilistic Pushdown Automata and Visibly Pushdown Languages and CaRet; LOGIC;

D O I：

10.46298/lmcs-19(4:24)2023

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices and recursive procedures. Temporal properties are useful for specifying the chronological order of events during program execution. Existing approaches for model checking pPDA against temporal properties have focused mostly on omega-regular and LTL properties. In this paper, we give decidability and complexity results for the model checking problem of pPDA against omega-visibly pushdown languages that can be described by specification logics such as CaRet. These logical formulae allow specifying properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties such as total and partial correctness.

引用

页数：30

共 41 条

[1]

Alur R, 2004, LECT NOTES COMPUT SC, V2988, P467

[2]

Alur R., 2004, STOC 04, P202, DOI [10.1145/1007352.1007390, DOI 10.1145/1007352.1007390]

[3] First-order and temporal logics for nested words [J].

Alur, Rajeev ;

Arenas, Marcelo ;

Barcelo, Pablo ;

Etessami, Kousha ;

Immerman, Neil ;

Libkin, Leonid .

22ND ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2007, :151-+

[4]

Alur Rajeev, 2018, Handbook of Model Checking, P541, DOI [DOI 10.1007/978-3-319-10575-8, 10.1007/978-3-319-10575-8_17, DOI 10.1007/978-3-319-10575-817]

[5]

Ash R., 2000, Probability and Measure Theory, V2nd

[6] Proofs of randomized algorithms in COQ [J].

Audebaud, Philippe ;

Paulin-Mohring, Christine .

SCIENCE OF COMPUTER PROGRAMMING, 2009, 74 (08) :568-589

[7]

Axelrod David, 2015, Branching Processes in Biology, DOI DOI 10.1007/978-1-4939-1559-0

[8]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[9] Probabilistic Relational Reasoning for Differential Privacy [J].

Barthe, Gilles ;

Koepf, Boris ;

Olmedo, Federico ;

Zanella-Beguelin, Santiago .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2013, 35 (03)

[10] Visibly Linear Temporal Logic [J].

Bozzelli, Laura ;

Sanchez, Cesar .

JOURNAL OF AUTOMATED REASONING, 2018, 60 (02) :177-220

← 1 2 3 4 5 →