<div class="csl-bib-body">
<div class="csl-entry">Pontiggia, F., Bartocci, E., & Chiari, M. (2025). POPACheck: A Model Checker for Probabilistic Pushdown Automata. In R. Piskac & Z. Rakamaric (Eds.), <i>Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part II</i> (pp. 105–121). Springer. https://doi.org/10.1007/978-3-031-98679-6_5</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/218189
-
dc.description.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
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
Probabilistic Model Checking
en
dc.subject
Pushdown Model Checking
en
dc.subject
Temporal Logic
en
dc.subject
Operator Precedence Languages
en
dc.title
POPACheck: A Model Checker for Probabilistic Pushdown Automata
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.editoraffiliation
Yale University, United States of America (the)
-
dc.relation.isbn
978-3-031-98679-6
-
dc.relation.issn
0302-9743
-
dc.description.startpage
105
-
dc.description.endpage
121
-
dc.relation.grantno
101107303
-
dc.relation.grantno
101034440
-
dc.relation.grantno
ICT22-023
-
dc.relation.grantno
ICT19-018
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part II
-
tuw.container.volume
15932
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Springer
-
tuw.project.title
COntext-free model checking for Recursive PrObabilistic pRogrAms
-
tuw.project.title
Logics for Computer Science Program at TU Wien
-
tuw.project.title
Training and Guiding AI Agents with Ethical Rules
-
tuw.project.title
Distribution Recovery for Invariant Generation of Probabilistic Programs
-
tuw.researchTopic.id
I2
-
tuw.researchTopic.name
Computer Engineering and Software-Intensive Systems
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E191-01 - Forschungsbereich Cyber-Physical Systems
-
tuw.publication.orgunit
E056-13 - Fachbereich LogiCS
-
tuw.publication.orgunit
E056-17 - Fachbereich Trustworthy Autonomous Cyber-Physical Systems
-
tuw.publication.orgunit
E056-26 - Fachbereich Automated Reasoning
-
tuw.publisher.doi
10.1007/978-3-031-98679-6_5
-
dc.description.numberOfPages
17
-
tuw.author.orcid
0000-0003-2569-6238
-
tuw.author.orcid
0000-0002-8004-6601
-
tuw.author.orcid
0000-0001-7742-9233
-
tuw.editor.orcid
0000-0002-3267-0776
-
tuw.editor.orcid
0000-0001-7946-0162
-
tuw.event.name
37th International Conference Computer Aided Verification (CAV 2025)
en
tuw.event.startdate
21-07-2025
-
tuw.event.enddate
25-07-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Zagreb
-
tuw.event.country
HR
-
tuw.event.presenter
Pontiggia, Francesco
-
tuw.event.track
Multi Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Elektrotechnik, Elektronik, Informationstechnik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
2020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
50
-
wb.sciencebranch.value
40
-
wb.sciencebranch.value
10
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.fulltext
no Fulltext
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.grantfulltext
none
-
crisitem.author.dept
E191-01 - Forschungsbereich Cyber-Physical Systems
-
crisitem.author.dept
E191-01 - Forschungsbereich Cyber-Physical Systems
-
crisitem.author.dept
E191-01 - Forschungsbereich Cyber-Physical Systems
-
crisitem.author.orcid
0000-0003-2569-6238
-
crisitem.author.orcid
0000-0002-8004-6601
-
crisitem.author.orcid
0000-0001-7742-9233
-
crisitem.author.parentorg
E191 - Institut für Computer Engineering
-
crisitem.author.parentorg
E191 - Institut für Computer Engineering
-
crisitem.author.parentorg
E191 - Institut für Computer Engineering
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
crisitem.project.funder
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
