Table of Contents
All contents
In this page, it is easy to search something in all contents.Back to Start page
Talks on Logics
In these talks the students present papers on temporal logics (LTL, CTL, CTL*, μ-Calculus, …). Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| On characterization of safety and liveness properties in temporal logic | A.P. Sistla | paper |
| Recognizing safety and liveness | B. Alpern and F.B. Schneider | paper |
| Expressibility results for linear-time and branching-time logics | E.M. Clarke and I.A. Draghicescu | paper |
| Counterexample-preserving reduction for symbolic model checking | Liu et. al. | paper |
| The common fragment of CTL and LTL | M. Maidl | paper |
| Alternating tree automata, parity games, and modal μ-calculus | T. Wilke | paper |
| Results on the propositional μ-calculus | D. Kozen | paper, paper |
| A finite model theorem for the propositional μ-calculus | D. Kozen | paper |
| A proof system for the linear time μ-calculus | C. Dax, M. Hofmann, and M. Lange | paper |
| Automata and fixed point logic: a coalgebraic perspective | Y. Venema | paper |
| Axiomatising linear time μ-calculus | R. Kaivola | paper |
| Temporal logic with fixed points | B. Banieqbal and H. Barringer | paper |
| Translating CTL* into the modal μ-calculus | M. Dam | paper |
| On the universal and existential fragments of the μ-calculus | T.A. Henziger, O. Kupferman, and R. Majumdar | paper |
| An automata theoretic decision procedure for the propositional μ-calculus | R.S. Street and E.A. Emerson | paper |
| A linear translation from CTL* to first-order modal μ-calculus | S. Cranen, J.F. Groote, and M. Reniers | paper |
| Model checking and the μ-calculus | E.A. Emerson | paper |
| Completeness of Kozen's axionatization for the modal μ-calculus: a simple proof | K. Tamura | paper |
| A recursive probabilistic temporal logic | P.F. Castro, C. Kilmurray, and N. Piterman | paper |
| Parametric Linear Dynamic Logic | P. Faymonville and M. Zimmermann | paper |
| The Temporal Logic of Actions | Leslie Lamport | paper |
Talks on Automata
In these talks the students present papers on automata theory. Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| Families of DFAs as Acceptors of ω-Regular Languages | D. Angluin, U. Boker and D. Fisman | paper |
Talks on BDDs
In these talks the students present papers on BDD based solution techniques. Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| Multi-terminal binary decision diagrams: an efficient data structure for matrix representation | M. Fujita, P.C. McGeer, and J.C.-Y. Yang | paper |
Talks on Bisimulation
In these talks the students present papers on bisimulations algorithms. Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| When simulation meets antichain (on checking language inclusion of NFAs) | Abdulla et. al. | paper |
| Bisimulation minimization in O(m log n) time | A. Valmari | paper |
| Three partition refinement algorithms | R. Paige and R.E. Tarjan | paper |
| Checking NFA equivalence with bisimulations up to congruence | F. Bonchi and D. Pous | paper |
| An O(m log n) algorithm for stuttering equivalence and branching bisimulation | J.F. Groote and A. Wijs | paper |
Talks on Learning Algorithms
In these talks the students present papers on learning algorithms.Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| Learning regular sets from queries and counterexamples | D. Angluin | paper |
| PAC learning-based verification and model synthesis | Chen et. al. | paper |
| Learning behaviors of automata from multiplicity and equivalence queries | F. Bergadano and S. Varricchio | paper |
| Learning functions represented as multiplicity automata | Beimel et. al. | paper |
| Learning ordered binary decision diagrams | R. Gavaldà and D. Guijarro | paper |
| Angluin-style learning of NFA | Bolling et. al. | paper |
| Learning regular automata via alternating automata | D. Angluin, S. Eisenstat, and D. Fisman | paper |
| An efficient query learning algorithm for ordered binary decision diagrams | A. Nakamura | paper |
Talks on Model-Checking Book
In these talks the students present the chapters of the Baier-Katoen “Principle of Model Checking” book and Manna-Pnueli “The temporal logic of reactive and concurrent systems” book Back to Start page or Back to Top
| Title | Slides |
|---|---|
| Regular properties, part I: regular safety properties | slides |
| Regular properties, part II: ω-regular properties | slides |
| Regular properties: part III: model checking with Büchi automata | slides |
| Linear Temporal Logic (LTL), part I: syntax and semantics of LTL | slides |
| Linear Temporal Logic (LTL), part II: automata-based LTL model checking | slides |
| Linear Temporal Logic (LTL), part III: complexity of LTL model checking | slides |
| Computation Tree Logic (CTL), part I: syntax and semantics of CTL | slides |
| Computation Tree Logic (CTL), part II: expressiveness of CTL and LTL | slides |
| Computation Tree Logic (CTL), part III: CTL model checking | slides |
| Computation Tree Logic (CTL), part IV: CTL with fairness | slides |
| Computation Tree Logic (CTL), part V: CTL+ and CTL* | slides |
Talks on Classical Verification
In these talks we consider the problem of verification in classical setting.Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| Learning Assumptions for Compositional Verification | Jamieson M. Cobleigh, Dimitra Giannakopoulou, and Corina S. Păsăreanu | paper |
Talks on Probabilistic Verification
In these talks we consider the problem of probabilistic verification .Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| Compositional Verification of Probabilistic Systems using Learning | Lu Feng, Marta Kwiatkowska and David Parker | paper |
| Compositional Probabilistic Verification through Multi-Objective Model Checking | M. Kwiatkowska et al. | paper |
| Automated Learning of Probabilistic Assumptions for Compositional Reasoning | Lu Feng, Marta Kwiatkowska, and David Parker | paper |
Talks on Probabilistic Planning
In these talks we consider the problem of planning on probabilistic systems in order to satisfy given properties or optimizing some reward.Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| RDDL language description | Scott Sanner | RDDL, Sanner's slides |
| Trial-based Heuristic Tree Search for Finite Horizon MDPs | THTS(long version), THTS(short version), PROST paper | |
| Gourmand and UCT | UCT/PROST, Gourmand | |
| Plannig with first-order TEP goals | J.A. Baier and S. A. McIlraith | paper |
Talks on Probabilistic Hybrid Planning
In these talks we consider several problems related to hybrid systems, such as model checking, planning, and so on.Back to Start page or Back to Top
Talks on Generic Topics
In these talks the students present papers on a variety of topics.Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| Faster and dynamic algorithms for maximal end-components decomposition and related graph problems in probabilistic verification | K. Chatterjee and M. Henzinger | paper |
| Fixed points vs. infinite generation | D. Niwiński | paper |
| Hacking nondeterminism with induction and coinduction | F. Bonchi and D. Pous | paper |
| First-order definable languages | V. Diekert and P. Gastin | paper |
| Infinite games played on finite graphs | R. McNaughton | paper |
| A deterministic subexponential algorithm for solving parity games | M. Jurdziński, M. Paterson, and U. Zwich | paper |
| The equivalence problem for regular expressions with squaring requires exponential space | A.R. Meyer and L.J. Stockmeyer | paper |
| Safra's determinization construction | K. Kumar | paper |
Software Engineering
In these talks we consider some topics in software engineering.Back to Start page or Back to Top
| Title | Authors | Reference Papers |
|---|---|---|
| Mining Sandboxes | K. Jamrozik, P. von Styp-Rekowsky, A. Zeller | paper |
Talks on Other Interesting Topics
In these talks we consider other problems related to probabilistic systems that do not fit in the previous categories.Back to Start page or Back to Top