BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Date iCal//NONSGML kigkonsult.se iCalcreator 2.20.2//
METHOD:PUBLISH
X-WR-CALNAME;VALUE=TEXT:Eventi DIAG
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:STANDARD
DTSTART:20181028T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20191027T030000
TZNAME:CET
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20190331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:calendar.18156.field_data.0@www.ugov-ricerca.uniroma1.it
DTSTAMP:20260413T202539Z
CREATED:20190326T185404Z
DESCRIPTION:Synthesis from temporal specifications is a fundamental problem
  in Artificial Intelligence and Computer Science. A popular specification 
 is Linear Temporal Logic (LTL). The standard approach to solving LTL synth
 esis requires\, however\, determinization of automata on infinite words an
 d solving parity games\, both challenging algorithmic problems. Thus a maj
 or barrier of temporal synthesis has been algorithmic difficulty. One appr
 oach to combating this difficulty is  to focus on using fragments of LTL\,
  for which synthesis problems are simpler.  A new logic for temporal synth
 esis\, called LTLf \, was proposed recently by De Giacomo and Vardi. The f
 ocus there is not on limiting the syntax of LTL\, but on interpreting it s
 emantically on finite traces\, rather than infinite traces. Such interpret
 ation allows the executions being arbitrarily long\, but not infinite\, an
 d is adequate for finite-horizon planning problems. While limiting the sem
 antics to finite traces does not change the computational complexity of te
 mporal synthesis (2EXPTIME)\, the algorithms are much simpler. The reason 
 is that those algorithms require determinization of automata on finite wor
 ds (rather than infinite words)\, and solving reachability games (rather t
 han parity games). Another application\, is that temporal synthesis of Saf
 ety LTL formulas\, a syntactic fragment of LTL expressing safety propertie
 s\, can be reduced to reasoning about finite words. This approach has been
  implemented in a tool Syft for LTLf synthesis and in SSyft for synthesis 
 of Safety LTL formulas\, and has been shown to outperform existing tempora
 l-synthesis tools such as Unbeast and Acacia+.Short bio: Shufang Zhu is a 
 PhD student in the School of Computer Science and Software Engineering at 
 East China Normal University. She is advised by Prof. Geguang Pu and Prof.
  Moshe Vardi from Rice University. Her works are in formal verification an
 d synthesis\, specifically focusing on developing techniques for synthesis
  from temporal specifications.
DTSTART;TZID=Europe/Paris:20190401T170000
DTEND;TZID=Europe/Paris:20190401T170000
LAST-MODIFIED:20200212T024047Z
LOCATION:Via Ariosto 25\, Aula A7
SUMMARY:Shufang Zhu -  Temporal Synthesis with Reachability and Safety Goal
 s - Shufang Zhu (School of Computer Science and Software Engineering at Ea
 st China Normal University)
URL;TYPE=URI:http://www.ugov-ricerca.uniroma1.it/node/18156
END:VEVENT
END:VCALENDAR