BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:88f48435-7d9e-42a1-b85f-03a1752255ba
X-WR-CALNAME:[MTV] Déborah Boyenval  (U. Côte d'Azur) - Formal modeling of 
 the discrete dynamics of intrinsic cell cycle checkpoints: a proof of conc
 ept
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20251026T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20241027T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20230326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20240331T020000
RDATE:20250330T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:88f48435-7d9e-42a1-b85f-03a1752255ba
DTSTAMP:20260407T074449Z
CLASS:PUBLIC
DESCRIPTION:The cell cycle is a sequence of events by which a cell reproduc
 es itself while preserving the integrity of its genome. This preservation 
 property is ensured by a set of biological regulatory mechanisms called ch
 eckpoints\, mainly described as arrest phenomenon observed in the context 
 of DNA damage. This phenomenon is the consequence of the /temporal separat
 ion of the phases/ of the cell cycle that\, to the best of our knowledge\,
  has never been formalized.\nTo address this emerging issue\, we propose a
 n updated discrete model of the mammalian cell cycle progression including
  G1\, S\, G2\, M and G0 quiescence phases\, as well as a methodology for f
 ormalizing a phase in order to verify their temporal separation. Opting fo
 r René Thomas' modeling framework leads the way to /an enriched Hoare/ log
 ic to compute /an biologically admissible/ part of each phase within an as
 ynchronous state transition graph.\nTwo phases are temporally isolated if 
 and only if i) there is a René Thomas' model (i.e. a parametrization of an
  influence graph) such that any event that can end a phase is required bef
 ore any event that can initiate the next phase and ii) there is no path fr
 om an incomplete phase to the next phase. This satisfiability problem has 
 been resolved using Prolog and TotemBioNet\, a software platform to suppor
 t the design of René Thomas' models with CTL model-checking and Hoare logi
 c.
DTSTART;TZID=Europe/Paris:20231109T130000
DTEND;TZID=Europe/Paris:20231109T140000
LOCATION:salle 178\, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Déborah Boyenval  (U. Côte d'Azur) - Formal modeling of the d
 iscrete dynamics of intrinsic cell cycle checkpoints: a proof of concept
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
