Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
142 | Michael Huth 0001, Nir Piterman, Daniel Wagner 0002 |
Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL. |
FCT |
2009 |
DBLP DOI BibTeX RDF |
|
122 | Frank Ciesinski, Marcus Größer |
On Probabilistic Computation Tree Logic. |
Validation of Stochastic Systems |
2004 |
DBLP DOI BibTeX RDF |
PCTL, PCTL*, probabilistic deterministic systems, probabilistic nondeterministic systems, quantitative model checking, scheduler, fairness, Markov decision processes, discrete time Markov chains |
109 | Harald Fecher, Michael Huth 0001, Nir Piterman, Daniel Wagner 0002 |
Hintikka Games for PCTL on Labeled Markov Chains. |
QEST |
2008 |
DBLP DOI BibTeX RDF |
|
104 | Federico Ramponi, Debasish Chatterjee, Sean Summers, John Lygeros |
On the connections between PCTL and dynamic programming. |
HSCC |
2010 |
DBLP DOI BibTeX RDF |
pctl, dynamic programming, markov processes, integral equation |
99 | Tomás Brázdil, Vojtech Forejt, Jan Kretínský, Antonín Kucera 0001 |
The Satisfiability Problem for Probabilistic CTL. |
LICS |
2008 |
DBLP DOI BibTeX RDF |
temporal logics, Markov chains |
99 | Krishnendu Chatterjee, Koushik Sen, Thomas A. Henzinger |
Model-Checking omega-Regular Properties of Interval Markov Chains. |
FoSSaCS |
2008 |
DBLP DOI BibTeX RDF |
|
82 | Ahmed Bouajjani, Rachid Echahed, Peter Habermehl |
Verifying Infinite State Processes with Sequential and Parallel Composition. |
POPL |
1995 |
DBLP DOI BibTeX RDF |
|
82 | Ahmed Bouajjani, Rachid Echahed, Riadh Robbana |
Verification of Nonregular Temporal Properties for Context-Free Processes. |
CONCUR |
1994 |
DBLP DOI BibTeX RDF |
|
66 | Tomás Brázdil, Vojtech Forejt |
Strategy Synthesis for Markov Decision Processes and Branching-Time Logics. |
CONCUR |
2007 |
DBLP DOI BibTeX RDF |
|
66 | Tomás Brázdil, Antonín Kucera 0001, Oldrich Strazovský |
On the Decidability of Temporal Properties of Probabilistic Pushdown Automata. |
STACS |
2005 |
DBLP DOI BibTeX RDF |
|
66 | Adnan Aziz, Vigyan Singhal, Felice Balarin |
It Usually Works: The Temporal Logic of Stochastic Systems. |
CAV |
1995 |
DBLP DOI BibTeX RDF |
|
66 | Andrea Bianco, Luca de Alfaro |
Model Checking of Probabalistic and Nondeterministic Systems. |
FSTTCS |
1995 |
DBLP DOI BibTeX RDF |
|
59 | Samik Basu 0001, Arka P. Ghosh, Ru He |
Approximate Model Checking of PCTL Involving Unbounded Path Properties. |
ICFEM |
2009 |
DBLP DOI BibTeX RDF |
|
59 | Josée Desharnais, Vineet Gupta 0001, Radha Jagadeesan, Prakash Panangaden |
Weak Bisimulation is Sound and Complete for PCTL*. |
CONCUR |
2002 |
DBLP DOI BibTeX RDF |
|
57 | Lars Grunske |
Specification patterns for probabilistic quality properties. |
ICSE |
2008 |
DBLP DOI BibTeX RDF |
csl, pctl, pctl*, probabilistic quality, probabilistic quality patterns, security, performance, reliability, safety, specification patterns |
49 | Arend Rensink |
Model Checking Quantified Computation Tree Logic. |
CONCUR |
2006 |
DBLP DOI BibTeX RDF |
|
49 | Christel Baier, Marta Z. Kwiatkowska |
Model Checking for a Probabilistic Branching Time Logic with Fairness. |
Distributed Comput. |
1998 |
DBLP DOI BibTeX RDF |
Probabilistic processes, Verification, Temporal logic, Fairness |
33 | Mouad Ben Mamoun, Nihal Pekergin |
Model Checking of Infinite State Space Markov Chains by Stochastic Bounds. |
ASMTA |
2008 |
DBLP DOI BibTeX RDF |
|
33 | Lijun Zhang 0001, Holger Hermanns, David N. Jansen |
Logic and Model Checking for Hidden Markov Models. |
FORTE |
2005 |
DBLP DOI BibTeX RDF |
|
33 | Marta Z. Kwiatkowska, Gethin Norman, David Parker 0001 |
Probabilistic symbolic model checking with PRISM: a hybrid approach. |
Int. J. Softw. Tools Technol. Transf. |
2004 |
DBLP DOI BibTeX RDF |
Binary decision diagrams, Symbolic model checking, Probabilistic model checking |
33 | Javier Esparza, Antonín Kucera 0001, Richard Mayr |
Model Checking Probabilistic Pushdown Automata. |
LICS |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli |
Bounded Probabilistic Model Checking with the Muralpha Verifier. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Xin Li 0010, Mizuhito Ogawa |
A Lightweight Mutual Authentication Based on Proxy Certificate Trust List. |
PDCAT |
2004 |
DBLP DOI BibTeX RDF |
Grid Computing, Mutual Authentication, Proxy Certificate |
33 | Marta Z. Kwiatkowska, Gethin Norman, David Parker 0001 |
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. |
TACAS |
2002 |
DBLP DOI BibTeX RDF |
|
33 | Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen, Marta Z. Kwiatkowska, Mark Ryan 0001 |
Symbolic Model Checking for Probabilistic Processes. |
ICALP |
1997 |
DBLP DOI BibTeX RDF |
|
26 | Miroslav Chodil, Antonín Kucera 0001 |
The satisfiability problem for a quantitative fragment of PCTL. |
J. Comput. Syst. Sci. |
2024 |
DBLP DOI BibTeX RDF |
|
26 | Massimo Bartoletti, Maurizio Murgia 0001, Roberto Zunino |
Sound approximate and asymptotic probabilistic bisimulations for PCTL. |
Log. Methods Comput. Sci. |
2023 |
DBLP DOI BibTeX RDF |
|
26 | Yang Liu 0265, Yan Ma, Yongsheng Yang |
A three-valued model abstraction framework for PCTL* stochastic model checking. |
Autom. Softw. Eng. |
2022 |
DBLP DOI BibTeX RDF |
|
26 | Yue Hao, Silu Huang, Xiaowen Xu |
Convergence of the PCTL algorithm for solving the discretized 3T energy equations in RHD problems. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
26 | Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, Jean-François Raskin |
Strategy Synthesis for Global Window PCTL. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
26 | Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, Jean-François Raskin |
Strategy Synthesis for Global Window PCTL. |
ICALP |
2022 |
DBLP DOI BibTeX RDF |
|
26 | Massimo Bartoletti, Maurizio Murgia 0001, Roberto Zunino |
A Sound Up-to-n, δ Bisimilarity for PCTL. |
COORDINATION |
2022 |
DBLP DOI BibTeX RDF |
|
26 | Massimo Bartoletti, Maurizio Murgia 0001, Roberto Zunino |
A Sound Up-to-$n$, $δ$ Bisimilarity for PCTL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
26 | Miroslav Chodil, Antonín Kucera 0001 |
The Satisfiability Problem for a Quantitative Fragment of PCTL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
26 | Miroslav Chodil, Antonín Kucera 0001 |
The Satisfiability Problem for a Quantitative Fragment of PCTL. |
FCT |
2021 |
DBLP DOI BibTeX RDF |
|
26 | Yu Wang 0044, Nima Roohi, Matthew West 0001, Mahesh Viswanathan 0001, Geir E. Dullerud |
Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
26 | Christel Baier, Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, Joachim Klein 0001 |
Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. |
Inf. Comput. |
2020 |
DBLP DOI BibTeX RDF |
|
26 | Yu Wang 0044, Nima Roohi, Matthew West 0001, Mahesh Viswanathan 0001, Geir E. Dullerud |
Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning. |
CDC |
2020 |
DBLP DOI BibTeX RDF |
|
26 | Yu Wang 0044, Nima Roohi, Matthew West 0001, Mahesh Viswanathan 0001, Geir E. Dullerud |
Statistical verification of PCTL using antithetic and stratified samples. |
Formal Methods Syst. Des. |
2019 |
DBLP DOI BibTeX RDF |
|
26 | Mathias Claus Jensen, Anders Mariegaard, Kim Guldstrand Larsen |
Symbolic Model Checking of Weighted PCTL Using Dependency Graphs. |
NFM |
2019 |
DBLP DOI BibTeX RDF |
|
26 | Darine Ameyed, Moeiz Miraoui, Atef Zaguia, Fehmi Jaafar, Chakib Tadj |
Using Probabilistic Temporal Logic PCTL and Model Checking for Context Prediction. |
Comput. Informatics |
2018 |
DBLP DOI BibTeX RDF |
|
26 | Yu Wang 0044, Nima Roohi, Matthew West 0001, Mahesh Viswanathan 0001, Geir E. Dullerud |
Statistical Verification of PCTL Using Stratified Samples. |
ADHS |
2018 |
DBLP DOI BibTeX RDF |
|
26 | Peter Baumgartner 0001, Sylvie Thiébaux, Felipe W. Trevizan |
Tableaux for Policy Synthesis for MDPs with PCTL* Constraints. |
CoRR |
2017 |
DBLP BibTeX RDF |
|
26 | Lisa Hutschenreiter, Christel Baier, Joachim Klein 0001 |
Parametric Markov Chains: PCTL Complexity and Fraction-free Gaussian Elimination. |
GandALF |
2017 |
DBLP DOI BibTeX RDF |
|
26 | Peter Baumgartner 0001, Sylvie Thiébaux, Felipe W. Trevizan |
Tableaux for Policy Synthesis for MDPs with PCTL* Constraints. |
TABLEAUX |
2017 |
DBLP DOI BibTeX RDF |
|
26 | Anders Mariegaard, Kim Guldstrand Larsen |
Symbolic Dependency Graphs for $$\text {PCTL}^{>}_{\le }$$ Model-Checking. |
FORMATS |
2017 |
DBLP DOI BibTeX RDF |
|
26 | Yang Liu, Xuandong Li, Yan Ma |
A Game-Based Approach for PCTL* Stochastic Model Checking with Evidence. |
J. Comput. Sci. Technol. |
2016 |
DBLP DOI BibTeX RDF |
|
26 | |
On the Hardness of PCTL Satisfiability. |
CoRR |
2015 |
DBLP BibTeX RDF |
|
26 | Diego Latella, Michele Loreti, Mieke Massink |
On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination. |
Sci. Comput. Program. |
2015 |
DBLP DOI BibTeX RDF |
|
26 | Xiaobin Zhang, Bo Wu 0005, Hai Lin 0002 |
Learning based supervisor synthesis of POMDP for PCTL specifications. |
CDC |
2015 |
DBLP DOI BibTeX RDF |
|
26 | Vahid Hashemi, Hassan Hatefi, Jan Krcál |
Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs (extended version). |
SynCoP |
2014 |
DBLP DOI BibTeX RDF |
|
26 | Tianrong Lin |
The complexity of model-checking of stateless probabilistic pushdown processes against PCTL. |
CoRR |
2014 |
DBLP BibTeX RDF |
|
26 | Yang Liu |
Game theory semantics for PCTL model checking label-extended probabilistic Petri net. |
ICIS |
2014 |
DBLP DOI BibTeX RDF |
|
26 | Lei Song 0001, Lijun Zhang 0001, Jens Chr. Godskesen |
Bisimulations Meet PCTL Equivalences for Probabilistic Automata |
Log. Methods Comput. Sci. |
2013 |
DBLP DOI BibTeX RDF |
|
26 | Alberto Puggelli, Wenchao Li 0001, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia |
Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. |
CAV |
2013 |
DBLP DOI BibTeX RDF |
|
26 | Nathalie Bertrand 0001, John Fearnley, Sven Schewe |
Bounded Satisfiability for PCTL |
CoRR |
2012 |
DBLP BibTeX RDF |
|
26 | Alessandro D'Innocenzo, Alessandro Abate, Joost-Pieter Katoen |
Robust PCTL model checking. |
HSCC |
2012 |
DBLP DOI BibTeX RDF |
|
26 | Johannes Hölzl, Tobias Nipkow |
Verifying pCTL Model Checking. |
TACAS |
2012 |
DBLP DOI BibTeX RDF |
|
26 | Nathalie Bertrand 0001, John Fearnley, Sven Schewe |
Bounded Satisfiability for PCTL. |
CSL |
2012 |
DBLP DOI BibTeX RDF |
|
26 | Morteza Lahijanian, Sean B. Andersson, Calin Belta |
Control of Markov decision processes from PCTL specifications. |
ACC |
2011 |
DBLP DOI BibTeX RDF |
|
26 | Lei Song 0001, Lijun Zhang 0001, Jens Chr. Godskesen |
Bisimulations Meet PCTL Equivalences for Probabilistic Automata. |
CONCUR |
2011 |
DBLP DOI BibTeX RDF |
|
26 | Ernst Moritz Hahn, Tingting Han 0001, Lijun Zhang 0001 |
Synthesis for PCTL in Parametric Markov Decision Processes. |
NASA Formal Methods |
2011 |
DBLP DOI BibTeX RDF |
|
26 | Harald Fecher, Michael Huth 0001, Nir Piterman, Daniel Wagner 0002 |
PCTL model checking of Markov chains: Truth and falsity as winning strategies in games. |
Perform. Evaluation |
2010 |
DBLP DOI BibTeX RDF |
|
26 | Josée Desharnais, Vineet Gupta 0001, Radha Jagadeesan, Prakash Panangaden |
Weak bisimulation is sound and complete for pCTL*. |
Inf. Comput. |
2010 |
DBLP DOI BibTeX RDF |
|
26 | Federico Ramponi, Debasish Chatterjee, Sean Summers, John Lygeros |
On the connections between PCTL and Dynamic Programming. |
CoRR |
2009 |
DBLP BibTeX RDF |
|
26 | Pedro Arturo Góngora, David A. Rosenblueth |
A Characterization of Mixed-Strategy Nash Equilibria in PCTL Augmented with a Cost Quantifier. |
CLIMA |
2009 |
DBLP DOI BibTeX RDF |
|
26 | Berteun Damman, Tingting Han 0001, Joost-Pieter Katoen |
Regular Expressions for PCTL Counterexamples. |
QEST |
2008 |
DBLP DOI BibTeX RDF |
|
26 | Mark Reynolds 0001 |
An axiomatization of PCTL*. |
Inf. Comput. |
2005 |
DBLP DOI BibTeX RDF |
|
26 | Michael Huth 0001, Marta Z. Kwiatkowska |
Comparing CTL and PCTL on labeled Markov chains. |
PROCOMET |
1998 |
DBLP BibTeX RDF |
|
16 | Kenneth Chan, Iman Poernomo |
Compositional Prediction of Timed Behaviour for Process Control Architecture. |
QoSA |
2009 |
DBLP DOI BibTeX RDF |
|
16 | Indranil Saha, Debapriyay Mukhopadhyay |
Quantitative Analysis of a Probabilistic Non-repudiation Protocol through Model Checking. |
ICISS |
2009 |
DBLP DOI BibTeX RDF |
|
16 | Suzana Andova, Sonja Georgievska |
On Compositionality, Efficiency, and Applicability of Abstraction in Probabilistic Systems. |
SOFSEM |
2009 |
DBLP DOI BibTeX RDF |
|
16 | Tomás Brázdil, Vojtech Forejt, Antonín Kucera 0001 |
Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives. |
ICALP (2) |
2008 |
DBLP DOI BibTeX RDF |
|
16 | Miguel E. Andrés, Peter van Rossum |
Conditional Probabilities over Probabilistic and Nondeterministic Systems. |
TACAS |
2008 |
DBLP DOI BibTeX RDF |
|
16 | Taolue Chen, Tingting Han 0001, Joost-Pieter Katoen |
Time-Abstracting Bisimulation for Probabilistic Timed Automata. |
TASE |
2008 |
DBLP DOI BibTeX RDF |
time-abstracting bisimulation, probabilistic timed automata |
16 | Luca de Alfaro, Krishnendu Chatterjee, Marco Faella, Axel Legay |
Qualitative Logics and Equivalences for Probabilistic Systems. |
QEST |
2007 |
DBLP DOI BibTeX RDF |
|
16 | Marcin Jurdzinski, François Laroussinie, Jeremy Sproston |
Model Checking Probabilistic Timed Automata with One or Two Clocks. |
TACAS |
2007 |
DBLP DOI BibTeX RDF |
|
16 | Taolue Chen, Jian Lu 0001 |
Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm. |
FSKD (2) |
2007 |
DBLP DOI BibTeX RDF |
|
16 | Tomás Brázdil, Václav Brozek, Vojtech Forejt, Antonín Kucera 0001 |
Stochastic Games with Branching-Time Winning Objectives. |
LICS |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Harald Fecher, Martin Leucker, Verena Wolf |
Don't Know in Probabilistic Systems. |
SPIN |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Alastair F. Donaldson, Alice Miller 0001 |
Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives. |
ATVA |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Koushik Sen, Mahesh Viswanathan 0001, Gul Agha |
Model-Checking Markov Chains in the Presence of Uncertainties. |
TACAS |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Tomás Brázdil, Václav Brozek, Vojtech Forejt, Antonín Kucera 0001 |
Reachability in Recursive Markov Decision Processes. |
CONCUR |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Joost-Pieter Katoen, Maneesh Khattri, Ivan S. Zapreev |
A Markov Reward Model Checker. |
QEST |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Antonín Kucera 0001, Oldrich Strazovský |
On the Controller Synthesis for Finite-State Markov Decision Processes. |
FSTTCS |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Kenneth Chan, Iman Poernomo, Heinz W. Schmidt, Jane Jayaputera |
A Model-Oriented Framework for Runtime Monitoring of Nonfunctional Properties. |
QoSA/SOQUA |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Iman Poernomo, Jane Jayaputera, Heinz W. Schmidt |
Timed Probabilistic Constraints over the Distributed Management Taskforce Common Information Model. |
EDOC |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Conrado Daws |
Symbolic and Parametric Model Checking of Discrete-Time Markov Chains. |
ICTAC |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Jane Jayaputera, Iman Poernomo, Heinz W. Schmidt |
Runtime Verification of Timing and Probabilistic Properties using WMI and .NET. |
EUROMICRO |
2004 |
DBLP DOI BibTeX RDF |
|
16 | David N. Jansen, Holger Hermanns, Joost-Pieter Katoen |
A Probabilistic Extension of UML Statecharts. |
FTRTFT |
2002 |
DBLP DOI BibTeX RDF |
model checking, semantics, probabilities, Markov decision processes, UML statecharts |
16 | Danièle Beauquier, Alexander Moshe Rabinovich, Anatol Slissenko |
A Logic of Probability with Decidable Model-Checking. |
CSL |
2002 |
DBLP DOI BibTeX RDF |
|
16 | Marta Z. Kwiatkowska, Gethin Norman, David Parker 0001 |
PRISM: Probabilistic Symbolic Model Checker. |
Computer Performance Evaluation / TOOLS |
2002 |
DBLP DOI BibTeX RDF |
|
16 | Mark Reynolds 0001 |
More Past Glories. |
LICS |
2000 |
DBLP DOI BibTeX RDF |
temporal logic, automata, axiomatizations |
16 | Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Edmund M. Clarke |
ProbVerus: Probabilistic Symbolic Model Checking. |
ARTS |
1999 |
DBLP DOI BibTeX RDF |
|