====== All contents ======
In this page, it is easy to search something in all contents.[[start|Back to Start page]]
----

====== Talks on Logics ======
In these talks the students present papers on temporal logics (LTL, CTL, CTL*, μ-Calculus, ...).
[[start|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|{{:papers:p39-sistla.pdf|paper}} |
|Recognizing safety and liveness	|B. Alpern and F.B. Schneider	|{{:papers:RecSafeLive.pdf|paper}}|
|Expressibility results for linear-time and branching-time logics	|E.M. Clarke and I.A. Draghicescu	|{{:Papers:clarke.pdf|paper}}|
|Counterexample-preserving reduction for symbolic model checking	|Liu et. al.|{{:Papers:liu.pdf|paper}}|
|The common fragment of CTL and LTL	|M. Maidl	|{{:Papers:maidl.pdf|paper}}|
|Alternating tree automata, parity games, and modal μ-calculus	|T. Wilke	|{{:Papers:wilke.pdf|paper}}|
|Results on the propositional μ-calculus	|D. Kozen	|{{:Papers:kozen83.pdf|paper}}, {{:Papers:kozen-82-mu.pdf|paper}}|
|A finite model theorem for the propositional μ-calculus	|D. Kozen	|{{:Papers:kozen03.pdf|paper}}|
|A proof system for the linear time μ-calculus	|C. Dax, M. Hofmann, and M. Lange	|{{:Papers:dax06.pdf|paper}}|
|Automata and fixed point logic: a coalgebraic perspective	|Y. Venema	|{{:Papers:venema05.pdf|paper}}|
|Axiomatising linear time μ-calculus	|R. Kaivola	|{{:Papers:kaivola95.pdf|paper}}|
|Temporal logic with fixed points	|B. Banieqbal and H. Barringer	|{{:Papers:banieqbal.pdf|paper}}|
|Translating CTL* into the modal μ-calculus	|M. Dam	|{{:Papers:dam90.pdf|paper}}|
|On the universal and existential fragments of the μ-calculus	|T.A. Henziger, O. Kupferman, and R. Majumdar	|{{:Papers:henzinger-mu-Exis-Universal.pdf|paper}}|
|An automata theoretic decision procedure for the propositional μ-calculus	|R.S. Street and E.A. Emerson	|{{:Papers:prop-mu-calculus89.pdf|paper}}|
|A linear translation from CTL* to first-order modal μ-calculus	|S. Cranen, J.F. Groote, and M. Reniers	|{{:Papers:ltl-mu-linear.pdf|paper}}|
|Model checking and the μ-calculus	|E.A. Emerson	|{{:Papers:mc-mu.pdf|paper}}|
|Completeness of Kozen's axionatization for the modal μ-calculus: a simple proof	|K. Tamura|{{:papers:mu-completeness-simple-proof.pdf|paper}}|
|A recursive probabilistic temporal logic|P.F. Castro, C. Kilmurray, and N. Piterman|{{:Papers:recursivePCTL.pdf|paper}}|
|Parametric Linear Dynamic Logic|P. Faymonville and M. Zimmermann|{{:Papers:pldl-fz-2015.pdf|paper}}|
|The Temporal Logic of Actions| Leslie Lamport|{{:Papers:lamport-actions-tplas00.pdf|paper}}|
====== Talks on Automata ======
In these talks the students present papers on automata theory.
[[start|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|{{:papers:abf-fdfa-mfcs16.pdf|paper}}| 

====== Talks on BDDs ======
In these talks the students present papers on BDD based solution techniques.
[[start|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|{{:Papers:mtbdd-data-structure.pdf|paper}}|

====== Talks on Bisimulation ======
In these talks the students present papers on bisimulations algorithms.
[[start|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.|{{:Papers:tacas10.pdf|paper}}|
|Bisimulation minimization in O(m log n) time	|A. Valmari	|{{:Papers:bisimulation.pdf|paper}}|
|Three partition refinement algorithms	|R. Paige and R.E. Tarjan	|{{:Papers:3partref.pdf|paper}}|
|Checking NFA equivalence with bisimulations up to congruence	|F. Bonchi and D. Pous	|{{:Papers:hkc.pdf|paper}}|
|An O(m log n) algorithm for stuttering equivalence and branching bisimulation	|J.F. Groote and A. Wijs	|{{:Papers:mlogn-stutter-bisimulation.pdf|paper}}|

====== Talks on Learning Algorithms ======
In these talks the students present papers on learning algorithms.[[start|Back to Start page]] or Back to [[|Top]]
----
^Title ^ Authors ^ Reference Papers ^
|Learning regular sets from queries and counterexamples	|D. Angluin	|{{:Papers:angluin87.pdf|paper}}|
|PAC learning-based verification and model synthesis	|Chen et. al.|{{:Papers:draft.pdf|paper}}|
|Learning behaviors of automata from multiplicity and equivalence queries	|F. Bergadano and S. Varricchio	|{{:Papers:learning-bergadano.pdf|paper}}|
|Learning functions represented as multiplicity automata	|Beimel et. al.|{{:Papers:learning-beimel.pdf|paper}}|
|Learning ordered binary decision diagrams	|R. Gavaldà and D. Guijarro	|{{:Papers:learning-OBDD.pdf|paper}}|
|Angluin-style learning of NFA	|Bolling et. al.	|{{:Papers:BHKL-ijcai09.pdf|paper}}|
|Learning regular automata via alternating automata	|D. Angluin, S. Eisenstat, and D. Fisman	|{{:Papers:aef-ijcai15.pdf|paper}}|
|An efficient query learning algorithm for ordered binary decision diagrams|A. Nakamura|{{:papers:learn-bdd.pdf|paper}}|

====== Talks on Model-Checking Book ======
In these talks the students present the chapters of the Baier-Katoen "Principle of Model Checking" {{:books:baier-katoen.pdf|book}}
and Manna-Pnueli "The temporal logic of reactive and concurrent systems" {{:books:manna-pnueli.pdf|book}}
[[start|Back to Start page]] or Back to [[|Top]]
----

^Title ^ Slides ^
|Regular properties, part I: regular safety properties	|{{:Slides:lec08.pdf|slides}}|
|Regular properties, part II: ω-regular properties	|{{:Slides:lec09_10.pdf|slides}}|
|Regular properties: part III: model checking with Büchi automata	|{{:Slides:lec11.pdf|slides}}|
|Linear Temporal Logic (LTL), part I: syntax and semantics of LTL	|{{:Slides:lec12_13.pdf|slides}}|
|Linear Temporal Logic (LTL), part II: automata-based LTL model checking	|{{:Slides:lec14_15.pdf|slides}}|
|Linear Temporal Logic (LTL), part III: complexity of LTL model checking	|{{:Slides:lec15.pdf|slides}}|
|Computation Tree Logic (CTL), part I: syntax and semantics of CTL	|{{:Slides:lec17.pdf|slides}}|
|Computation Tree Logic (CTL), part II: expressiveness of CTL and LTL	|{{:Slides:lec18.pdf|slides}}|
|Computation Tree Logic (CTL), part III: CTL model checking	|{{:Slides:lec19.pdf|slides}}|
|Computation Tree Logic (CTL), part IV: CTL with fairness	|{{:Slides:lec20.pdf|slides}}|
|Computation Tree Logic (CTL), part V: CTL+ and CTL*	|{{:Slides:lec21_01.pdf|slides}}|

====== Talks on Classical Verification ======
In these talks we consider the problem of verification in classical setting.[[start|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|{{:papers:cgp-assume-tacas03.pdf|paper}}|

====== Talks on Probabilistic Verification ======
In these talks we consider the problem of probabilistic verification .[[start|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|{{:papers:fkp-comp-learn-qest10.pdf|paper}}|
|Compositional Probabilistic Verification through Multi-Objective Model Checking|M. Kwiatkowska et al.|{{:papers:knpq-multiobj-ic13.pdf|paper}}|
|Automated Learning of Probabilistic Assumptions for Compositional Reasoning|Lu Feng, Marta Kwiatkowska, and David Parker|{{:papers:fkp-learn-comp-fase11.pdf|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.[[start|Back to Start page]] or Back to [[|Top]]
----
^Title ^ Authors ^ Reference Papers ^
|RDDL language description|Scott Sanner|{{:competitions:rddl.pdf|RDDL}}, {{:competitions:rddl-slides.pdf|Sanner's slides}}|
|Trial-based Heuristic Tree Search for Finite Horizon MDPs| |{{:competitions:keller-helmert-icaps2013.pdf|THTS(long version)}}, {{:Competitions:keller-helmert-rldm2013.pdf|THTS(short version)}}, {{:Competitions:keller-eyerich-icaps2012.pdf|PROST paper}}|
|Gourmand and UCT|   |{{:Competitions:keller-eyerich-icaps2012.pdf|UCT/PROST}},  {{:competitions:gourmand.pdf|Gourmand}}|
|Plannig with first-order TEP goals|J.A. Baier and S. A. McIlraith|{{:Papers:bai-mci-aaai06.pdf|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.[[start|Back to Start page]] or Back to [[|Top]]
----
^Title ^ Authors ^ Reference Papers ^
|Approximate model checking for stochastic hybrid systems|Abate et. al.|{{:Papers:AKLP10.pdf|paper}}|
|A stochastic games framework for verification and control of discrete time stochastic hybrid systems|Ding et. al|{{:Papers:DKSALT13.pdf|paper}}|

====== Talks on Generic Topics ======
In these talks the students present papers on a variety of topics.[[start|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|{{:Papers:faster_mecs.pdf|paper}}|
|Fixed points vs. infinite generation|D. Niwiński|{{:Papers:niwinski88.pdf|paper}}|
|Hacking nondeterminism with induction and coinduction|F. Bonchi and D. Pous|{{:Papers:p87-bonchi.pdf|paper}}|
|First-order definable languages|V. Diekert and P. Gastin|{{:papers:gastin-fo-definable.pdf|paper}}|
|Infinite games played on finite graphs|R. McNaughton|{{:Papers:game-mcnaughton.pdf|paper}}|
|A deterministic subexponential algorithm for solving parity games|M. Jurdziński, M. Paterson, and U. Zwich|{{:Papers:JPZ-subexpo-parity.pdf|paper}}|
|The equivalence problem for regular expressions with squaring requires exponential space|A.R. Meyer and L.J. Stockmeyer|{{:Papers:nba-equivalence.pdf|paper}}|
|Safra's determinization construction|K. Kumar|{{:Papers:safra-determinisation-lecture11.pdf|paper}}|

====== Software Engineering ======
In these talks we consider some topics in software engineering.[[start|Back to Start page]] or Back to [[|Top]]
----
^Title ^ Authors ^ Reference Papers ^
|Mining Sandboxes |K. Jamrozik, P. von Styp-Rekowsky, A. Zeller| {{:papers:jamrozik-mine-sandbox-icse16.pdf|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.[[start|Back to Start page]] or Back to [[|Top]]
----
^Title ^ Authors ^ Reference Papers ^
|Operational versus Weakest Pre-expectation Semantics for the Probabilistic Guarded Command Language|F. Gretz, J.-P. Katoen, A. McIver|{{:Papers:wpe-semantics.pdf|paper}}|
|Commutativity of reducers|Chen et. al.	|{{:Papers:reducers.pdf|paper}}|
|Slicing probabilistic programs | Hur et. al. |{{:Papers:slicing.pdf|paper}}|