~~NOCACHE~~
/* DO NOT EDIT THIS FILE               */
/* THIS FILE WAS GENERATED             */
/* EDIT THE FILE "indexheader" INSTEAD */
/* OR ACCESS THE DATABASE              */

{{page>.:indexheader}}

\\ ==== Next talks ====
[[en:seminaires:verif:index|Verification]]\\
Monday May 12, 2025, 11AM, 3052 and [[https://u-paris.zoom.us/j/87460234504?pwd=mVUPogiquRZpL0HxEVffccgKRTZ1ID.1|Zoom link]]\\
**Jeroen Keiren** (Eindhoven University of Technology) //An Expressive Timed Modal Mu-Calculus for Timed Automata//
<button type="link" size="xs" collapse="b11-2584">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b11-2584" collapsed="true">
<well size="sm">
In the untimed setting, it is well-known that the modal mu-calculus is more expressive than other modal logics such as LTL, CTL and CTL*. It can thus be considered a foundational logic for model-checking. In the timed setting, the status of similarly foundational logics is less satisfactory. There are timed extensions of modal logics, such as TCTL. Yet, the state of the art of timed mu-calculi is underdeveloped.
 
In this talk, I present a timed model mu-calculus $L_{rel}^{\mu,\nu}$ for encoding properties of systems modeled as timed automata. Our logic includes arbitrary fixpoints and an until-like modal operator for time elapses, and is shown to be strictly more expressive than existing timed modal mu-calculi introduced in the literature. It also enjoys decidable model checking, as it respects the traditional region-graph construction for timed automata. Additionally, I establish that, in contrast to other timed mu-calculi, $L_{rel}^{\mu,\nu}$ is strictly more expressive than Timed Computation Tree Logic (TCTL) in the setting of general timed automata, meaning that model checkers for $L_{rel}^{\mu,\nu}$ are immediately usable as model checkers for TCTL for general timed automata.
 
This is joint work with Rance Cleaveland and Peter Fontana, and appeared as [1].
 
[1] Cleaveland, R., Keiren, J.J.A., Fontana, P.: An Expressive Timed Modal Mu-Calculus for Timed Automata. In: Hillston, J. et al. (eds.) Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems., pp. 160–178. Springer Nature Switzerland, Cham (2024).
</well>
</collapse>


[[en:seminaires:verif:index|Verification]]\\
Monday June 23, 2025, 11AM, 3052 and [[https://u-paris.zoom.us/j/87460234504?pwd=mVUPogiquRZpL0HxEVffccgKRTZ1ID.1|Zoom link]]\\
**Sergio Yovine** (Universidad ORT Uruguay) //To be announced.//
\\


\\ ==== Previous talks ====
\\ === Year 2025 ===

{{page>.:verif2025}}

\\ === Year 2024 ===

{{page>.:verif2024}}

\\ === Year 2023 ===

{{page>.:verif2023}}

\\ === Year 2022 ===

{{page>.:verif2022}}

\\ === Year 2021 ===

{{page>.:verif2021}}

\\ === Year 2020 ===

{{page>.:verif2020}}

\\ === Year 2019 ===

{{page>.:verif2019}}

\\ === Year 2018 ===

{{page>.:verif2018}}

\\ === Year 2017 ===

{{page>.:verif2017}}

\\ === Year 2016 ===

{{page>.:verif2016}}