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.
This is a summary of the group meetings on 7 April, 2021
L*- Based Learning of Markov Decision Processes
They provide two algorithms to learn a given black-box Markov decision processes based on Angluin’s L* algorithm. They are exact learning and sample-based learning, respectively.
Q: What is for unambiguous?
A: The compatibility relation is not an equivalence relation, and a state may belong to more than one classes, which we call an ambiguous state, so for an unambiguous state, there is only one class whose representation is compatible with it.
Q: How to check equivalence in exact learning?
A: First it checks whether the hypothesis is isomophic to the model. If so, we only need finitely many output distribution queries to determine all the transition probabilities.
Q: Is there a quantitative description of the convergence?
A: Not yet in the paper. In the paper it only gives a convergence description based on Borel-Cantelli Lemma. It is interesting to consider its PAC guarantee description.
Q: Can MDP learning used for model checking and other field in software engineering?
A: There are some experiments in the paper. We need more investigation on this part.
This is a summary of the group meetings on 24 March, 2021
Efficient Certification of Spatial Robustness
这篇文章提出了一种计算范数约束向量场攻击的紧区间界限的新方法，使神经网络能够对向量场攻击进行验证。 首先是对每个像素的变换计算一个很紧的区间界，然后提出一个方法用线性平面去拟合这个上界和下界，也就是用线性平面计算它的凸松弛。并且展示了如何通过flow constraints来提供一个更紧的凸松弛。这种方法可以收紧对光滑向量场的松弛，并且可以和目前主流的鲁棒性验证器集成。
Congratulations to Junnan Xu who passed his Master thesis defense on Aug. 27th, 2020.
The title of his thesis is “An Axiomatisation of the Probabilistic μ-Calculus“.
The committee members are:
- Yuan Feng (chair)
- Wanwei Liu
- Zhilin Wu
- Naijun Zhan
Congratulations to Xuechao Sun who passed his Master thesis defense on May 23rd 2020.
The title of his thesis is “Synthesizing Nested Ranking Functions for Loop Programs via SVM“.
The committee members are:
- Yuan Feng (chair)
- Yi Li
- Zhilin Wu
- Lijun Zhang
LICS 2020 is co-organized by the Probabilistic Model Checking team at ISCAS and Dependable team at Saarland University.
For 2020, LICS is a virtual meeting, with talks, tutorials, and workshops given online.
The Journal of Computer Science & Technology, a CCF B ranked journal, is going to have a special section on software systems. Software systems have played critical roles in scientific research, business and society with research focuses on construction, operation, maintenance, and assessment of software systems. The special section is an effort to encourage and promote research to address challenges from the software systems perspective and its goal is to present the state-of-the-art and high-quality original research papers in the area of software systems.
The JCST’s special section of software systems covers two main themes:
- Internetware and Beyond, aiming to provide a forum where researchers and professionals from multiple disciplines and domains share ideas to explore and address the challenges brought by Internetware. It solicits submissions describing results of theoretical, empirical, conceptual, and experimental software engineering research related to Internetware.
- Dependable Software Engineering, soliciting submissions describing theoretical results, tools, and applications, related to applying formal methods in improving the quality of computer software and systems.
Accepted papers to the Dependable Software Engineering theme will be presented and discussed at the SETTA 2020 conference.
Papers need to be submitted before April 10, 2020; for more details about the themes, submission instructions and deadlines, see the official JCST CFP page.
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 who passed his PhD thesis defense on 1st November.
The title of the PhD thesis is “Novel Learning and Complementation Algorithms for Buchi Automata” .
The comittee members are:
- Lijun Zhang
- Moshe Vardi
- Naijun Zhan
- Sven Shewe
- Yih-Kuen Tsay
- Zhilin Wu