ePMC, the Extendible Probabilistic Model Checker, is now available publicly. It can be accessed online on GitHub, at this repository.
ePMC is the successor of IscasMC, from which it keeps all features about Linear Time Logic probabilistic model checking. ePMC is highly modular, which allows everyone to extend and improve the functionalities of the model checker.
When you cite our IscasMC model checker, please use [HahnLSTZ14].
Feel free to contact us by email if you find issues with the online model checker.
Title:Automata for Profit and Pleasure
Abstract:When admiring the beauty of automata, we look at their basic properties, like optimal transformations between different types and the principle costs they incur. But their beauty shouldn’t allow us to become blind to their usefulness, and when we want to profit, the questions change. For example, finer traits than alternating/nondeterministic/determinstic come to the fore: we want automata that are fit for purpose. The first time that this has been named explicitly was in the discussion of good-for-games automata, but it has occurred much earlier, e.g. (speaking as Lijun’s guest) in using limit determinism in the evaluation of MDPs.
There are more such examples, such as using mild subclasses of unambiguous automata for the evaluation of Markov chains, good-for-MDP automata, and good-for-small-games automata, that allow us to combine pleasure with profit—just like when one works in academia.
Sven Schewe, Bio:
I am a Professor at the Department of Computer Science of the University of Liverpool, where I lead the AI Section. I am a founding member and former leader of our Verification Group and have a secondary affiliation with the Algorithms, Complexity Theory and Optimisation Group. I am also affiliated with the Institute for Risk and Uncertainty.
I gained a Diplom degree in Computer Science (Diplom Informatiker) with a minor in Operations Research and Planning in 1997 from the University of the Federal Armed Forces Munich. Then I worked in the Command and Control Systems Command of the German Navy as a Systems Engineer in different fields of the analysis and construction of safety-critical systems, including the specification and construction of such systems as well as quality assurance and project management. To complement this, I gave myself a treat and studied Math at the FernUniversität in Hagen, earning a degree in Mathematics (Diplom Mathematiker) in 2004. Returning to education, I joined the Reactive Systems Group at the Department of Computer Science of Saarland University in 2004, and obtained a PhD (Dr. rer. nat.) in Computer Science in 2008, moving on to an academic position in Liverpool.
Title: Conventional Suggestions to the Automata-Theoretic Community
Abstract: For better communications, when presenting existing works or new findings, researchers follow established conventions, including preferred choices among alternative definitions, names, etc. Conventions may change and evolve over time. In this talk, I will suggest and justify three conventional changes to the theory of automata on which the automata-theoretic community heavily relies. The first and the second changes are about the initial setting and the computations of an automaton, while the third is about a complementation construction.
Yih-Kuen Tsay, Bio:
Dr. Yih-Kuen Tsay is a professor in the Department of Information Management at National Taiwan University. Dr. Tsay received his B.S. degree from National Taiwan University in 1984 and his M.S. and Ph.D. degrees from the University of California at Los Angeles in 1989 and 1993, all in Computer Science. In 1995, after two years as a postdoctoral research fellow at Uppsala University in Sweden, Dr. Tsay returned to Taiwan to join his current department. He was the department chair from 2013 to 2017.
Dr. Tsay is generally interested in rigorous methods and practically usable tools that help ensure correctness, safety, and security of computer software. In terms of specific areas, his research interests include formal verification, temporal logic, automata theory, and software security. Further information may be found on his personal homepage at http://im.ntu.edu.tw/~tsay/.
Title: Program Verification: a 50-Year History
Abstract: The year 2019 sees the 50th anniversary of Tony Hoare’s CACM paper, “An Axiomatic Basis for Compuer Programming”. In that paper, Hoare stated: “When the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program, and predict their properties with a confidence limited only by the reliability of the electronics.” In this talk, I will review the 50-year history of this vision, describing the obstacles, the controversies, and progress milestones. I will conclude with the description of both impressive progress and dramatic failures exhibited over the past few years.
The talk is accessible to general CS audience.
Moshe Vardi, Bio:
Moshe Y. Vardi is the George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology at Rice University. He is the recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS Distinguished Achievements Award, the Southeastern Universities Research Association’s Distinguished Scientist Award, and the Church Award. He is the author and co-author of over 500 papers, as well as two books: “Reasoning about Knowledge” and “Finite Model Theory and Its Applications”. He is a Fellow of the Association for Computing Machinery, the American Association for Artificial Intelligence, the American Association for the Advancement of Science, the European Association for Theoretical Computer Science, the Institute for Electrical and Electronic Engineers, and the Society for Industrial and Applied Mathematics. He is a member of the US National Academy of Engineering and National Academy of Science, the American Academy of Arts and Science, the European Academy of Science, and Academia Europaea. He holds honorary doctorates from the Saarland University in Germany, Orleans University in France, UFRGS in Brazil, and the University of Liege in Belgium. He is currently a Senior Editor of of the Communications of the ACM, after having served for a decade as Editor-in-Chief.
Congratulations to Yong Li on defending his PhD thesis titled “Novel Learning and Complementation Algorithms for Buchi Automata” on 1st November.
The comittee members are:
- Lijun Zhang
- Moshe Vardi
- Naijun Zhan
- Sven Shewe
- Yih-Kuen Tsay
- Zhilin Wu
The SETTA paper about the polynomial-time alternating probabilistic bisimulation for interval MDPs [HashemiTHHE17] has been awarded with the SETTA’17 best paper award.
Ralf Wimmer and Karina Wimmer, from Albert-Ludwigs-University Freiburg, Germany, visits us from Oct. 17 to Oct. 27, 2016. During the visit, Ralf gives a course on Symbolic Verification while Karima gives a talk on Dependency Quantified Boolean Formulas and Skolem functions applied to DQBF.
Arnd Hartmanns, from University of Twente, is visiting us from Sept. 5 to Sept. 14, 2016.
We are hosting the IscasMC summer school on the Practical Aspects on Probabilistic Model Checking, where we survey the main aspects relative to probabilistic model checking, with a specific attention to the practical aspects, in particular relative to the implementation of IscasMC.
See the official page for more details.