Record link: 
http://hdl.handle.net/20.500.12708/218189
-
Title: 
POPACheck: A Model Checker for Probabilistic Pushdown Automata
en
Citation: 
Pontiggia, F., Bartocci, E., & Chiari, M. (2025). POPACheck: A Model Checker for Probabilistic Pushdown Automata. In R. Piskac & Z. Rakamaric (Eds.), Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part II (pp. 105–121). Springer. https://doi.org/10.1007/978-3-031-98679-6_5
-
Publisher DOI: 
10.1007/978-3-031-98679-6_5
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Pontiggia, Francesco 
Bartocci, Ezio 
Chiari, Michele 
-
Organisational Unit: 
E191-01 - Forschungsbereich Cyber-Physical Systems 
E056-13 - Fachbereich LogiCS 
E056-17 - Fachbereich Trustworthy Autonomous Cyber-Physical Systems 
E056-26 - Fachbereich Automated Reasoning 
-
Published in: 
Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part II 
-
ISBN: 
978-3-031-98679-6
-
Volume: 
15932
-
Date (published): 
22-Jul-2025
-
Event name: 
37th International Conference Computer Aided Verification (CAV 2025) 
en
Event date: 
21-Jul-2025 - 25-Jul-2025
-
Event place: 
Zagreb, Croatia
-
Number of Pages: 
17
-
Publisher: 
Springer
-
Peer reviewed: 
Yes
-
Keywords: 
Probabilistic Model Checking; Pushdown Model Checking; Temporal Logic; Operator Precedence Languages
en
Abstract: 
We present POPACheck, the first model checking tool for probabilistic Pushdown Automata (pPDA) supporting temporal logic specifications. POPACheck provides a user-friendly probabilistic modeling language with recursion that automatically translates into Probabilistic Operator Precedence Automata (pOPA). pOPA are a class of pPDA that can express all the behaviors of probabilistic programs: sampling, conditioning, recursive procedures, and nested inference queries. On pOPA, POPACheck can solve reachability queries as well as qualitative and quantitative model checking queries for specifications in Linear Temporal Logic (LTL) and a fragment of Precedence Oriented Temporal Logic (POTL), a logic for context-free properties such as pre/post-conditioning.
en
Project title: 
COntext-free model checking for Recursive PrObabilistic pRogrAms: 101107303 (European Commission) 
Logics for Computer Science Program at TU Wien: 101034440 (European Commission) 
Training and Guiding AI Agents with Ethical Rules: ICT22-023 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) 
Distribution Recovery for Invariant Generation of Probabilistic Programs: ICT19-018 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) 
-
Research Areas: 
Computer Engineering and Software-Intensive Systems: 100%
-
Science Branch: 
1020 - Informatik: 50%
2020 - Elektrotechnik, Elektronik, Informationstechnik: 40%
1010 - Mathematik: 10%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

42
checked on Aug 14, 2025

Download(s)

3
checked on Aug 14, 2025

Google ScholarTM

Check