BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:4d77dcaa-3801-4637-872e-f7445d265428
X-WR-CALNAME:[MTV] Vaishnavi (CMI Chennai) -  Model-checking real-time syst
 ems: revisiting the alternating automaton route
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20270328T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20241027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20251026T030000
RDATE:20261025T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20250330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20260329T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:4d77dcaa-3801-4637-872e-f7445d265428
DTSTAMP:20260428T071409Z
CLASS:PUBLIC
DESCRIPTION:Alternating timed automata (ATA) are an extension of timed auto
 mata where the effect of each transition is described by a positive boolea
 n combination of (state-reset) pairs. Unlike classical timed automata\, AT
 As are closed under complementation and are therefore amenable to logic-to
 -automata translations. Several timed logics\, including Metric Temporal L
 ogic (MTL)\, can be converted to equivalent 1-clock ATA (1-ATAs). But curr
 ently\, tools for model checking timed systems don't use 1-ATAs directly i
 n computation\, and instead use sophisticated conversions to timed automat
 a instead. A reason for this could be that zone-based methods don't exist 
 for 1-ATAs\, unlike those extensively studied for TAs.\n\nOur goal is to i
 nitiate the study of zone-based algorithms directly for 1-ATAs. We first i
 ntroduce a deactivation operator to the 1-ATA syntax\, and using it define
  the class of bounded 1-ATAs. We then define a zone-based emptiness algori
 thm for 1-ATAs\, and look closely at the entailment relation that guarante
 es the termination of this algorithm.\n\nThis is a joint work with B. Sriv
 athsan and Patricia Bouyer that was accepted at FoSSaCS 2025.\n\n\nImport 
 automatique depuis https://framagenda.org/remote.php/dav/public-calendars/
 D3yqF7nwys9amfyY?export par sync_icals_to_drupal.py pour M2F
DTSTART;TZID=Europe/Paris:20250617T140000
DTEND;TZID=Europe/Paris:20250617T150000
LOCATION:Labri\, 178
SEQUENCE:0
SUMMARY:[MTV] Vaishnavi (CMI Chennai) -  Model-checking real-time systems: 
 revisiting the alternating automaton route
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
