“On-the-Fly Model Checking for Regular Alternation-Free Mu-Calculus” and “One Interface to Serve Them All”
Radu Mateescu and Jaco van de Pol,
INRIA Rhône-Alpes / University of Twente –
Abstract:
“On-the-Fly Model Checking for Regular Alternation-Free Mu-Calculus”: Model-checking is a successful technique for automatically verifying concurrent finite-state systems. When designing a model-checker, a good compromise must be made between the expressive power of the property description formalism, the complexity of the model-checking problem, and the user-friendliness of the interface. The logic we adopted is the regular alternation-free mu-calculus, an extension of the alternation-free mu-calculus with ACTL-like action formulas and PDL-like regular expressions, allowing a concise and intuitive description of safety, liveness, and (some) fairness properties over labelled transition systems (LTSs). The model-checking method consists in reformulating the verification problem as the local resolution of a boolean equation system (BES), which is carried out by linear-time algorithms based on various strategies (depth-first search, breadth-first search, etc.). These algorithms also generate full diagnostic information (examples and counterexamples) illustrating the truth value of temporal formulas. This method is at the heart of the EVALUATOR 3.5 model-checker of the CADP toolbox, developed using the generic OPEN/CAESAR environment for on-the-fly verification. The BES resolution algorithms are provided by the CAESAR_SOLVE library of OPEN/CAESAR.
“One Interface to Serve Them All” : I will explain a new interface for model checking tools, which enables o connect many model checking algorithms (explicit, distributed, symbolic, multi-core) to various input languages (Promela, mCRL, DVE). Also, several generic optimizations can be applied at the interface. Additionally, I will demonstrate the application of model checking to safety requirements of railway interlocking systems, in a project led by the UIC (Union Internationale des Chemins de Fer).
Date: 2010-May-17 Time: 15:00:00 Room: IST, Anfiteatro QA (Torre Sul)
For more information:
Upcoming Events
OLISSIPO Summer School in Lisbon | Computational phylogenetics to analyse the evolution of cells and communities
We are happy to announce the OLISSIPO Summer School on Computational phylogenetics to analyse the evolution of cells and communities, which will be held in Lisbon, Portugal, at INESC-ID, between July 2-7, 2023.
Keynote speakers:
David Posada, University of Vigo (class)
João Alves, University of Vigo (hands-on)
Nadia El-Mabrouk, Université de Montréal (class)
Mattéo Delabre, Université de Montréal (hands-on)
Ran Libeskind-Hadas, Claremont McKenna College (class and hands-on)
Russell Schwartz, Carnegie Mellon University (class and hands-on)
See the preliminary agenda at: https://olissipo.inesc-id.pt/tree-tango-school
Registration is mandatory. You can register at: https://forms.gle/VsASFHW5E7MJvaCc9
The registration fee is 250€ for students and OLISSIPO members and 350€ for postdocs or other researchers (meals indicated at the schedule of the school are included, accommodation and flights are not). All details will be made available upon registration.
We will have slots for flash talks (3-10 min depending on the number of submissions) to present yourself and the work you have been developing in your research.
The 13th Lisbon Machine Learning School | LxMLS 2023
The Lisbon Machine Learning Summer School (LxMLS) takes place yearly at Instituto Superior Técnico (IST). LxMLS 2023 will be a 6-day event (14-20 July, 2023), scheduled to take place as an in-person event.
The school covers a range of machine learning topics, from theory to practice, that are important in solving natural language processing problems arising in different application areas. It is organized jointly by Instituto Superior Técnico (IST), a leading Engineering and Science school in Portugal, the Instituto de Telecomunicações, the Instituto de Engenharia de Sistemas e Computadores, Investigação e Desenvolvimento em Lisboa (INESC-ID), the Lisbon ELLIS Unit for Learning and Intelligent Systems (LUMLIS), Unbabel, Zendesk, and IBM Research.
Check online for information about past editions: LxMLS 2011, LxMLS 2012, LxMLS 2013, LxMLS 2014, LxMLS 2015, LxMLS 2016, LxMLS 2017, LxMLS 2018, LxMLS 2019, LxMLS 2020, LxMLS 2021, LxMLS 2022 (you can also watch the videos of the lectures for 2016, 2017, 2018, and 2020).
31st International Conference on Information Systems Development (ISD 2023)
The 31st International Conference on Information Systems Development (ISD 2023) conference provides a forum for research and developments in the field of information systems. The theme of ISD 2023 is “Information systems development, organizational aspects and societal trends”. New trends in developing information systems emphasize the continuous collaboration between developers and operators in order to optimize the software delivery time. The conference promotes research on methodological and technological issues and how IS developers and operators are transforming organizations and society through information systems.
The ISD 2023 conference held this year also provides an opportunity for researchers and practitioners to promote their research, practical experience, and to discuss issues related to Information Systems through papers, posters, and journal-first paper presentations.
ISD 2023 will be hosted by Instituto Superior Técnico, in Lisbon, Portugal, on August 30–September 1, 2023.