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

{{page>.:indexheader}}

\\ ==== Prochaines séances ====
[[seminaires:verif:index|Vérification]]\\
Lundi 12 mai 2025, 11 heures, 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-2349">{{icon>info-circle?lg&color=#777}}</button>\\
<collapse id="b11-2349" 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>


[[seminaires:verif:index|Vérification]]\\
Lundi 23 juin 2025, 11 heures, 3052 and [[https://u-paris.zoom.us/j/87460234504?pwd=mVUPogiquRZpL0HxEVffccgKRTZ1ID.1|Zoom link]]\\
**Sergio Yovine** (Universidad ORT Uruguay) //Non encore annoncé.//
\\


\\ ==== Séances passées ====
\\ === Année 2025 ===

{{page>.:verif2025}}

\\ === Année 2024 ===

{{page>.:verif2024}}

\\ === Année 2023 ===

{{page>.:verif2023}}

\\ === Année 2022 ===

{{page>.:verif2022}}

\\ === Année 2021 ===

{{page>.:verif2021}}

\\ === Année 2020 ===

{{page>.:verif2020}}

\\ === Année 2019 ===

{{page>.:verif2019}}

\\ === Année 2018 ===

{{page>.:verif2018}}

\\ === Année 2017 ===

{{page>.:verif2017}}

\\ === Année 2016 ===

{{page>.:verif2016}}