BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260922T132555Z
UID:Seminar-ARK-523@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Louwe Kuijer:MAILTO:Louwe.Kuijer@liverpool.ac.uk
DTSTART:20190925T150000
DTEND:20190925T160000
SUMMARY:Argumentation and Representation of Knowledge Series
DESCRIPTION:Andrea Mazzullo: Do You Need Infinite Time?\n\nLinear temporal logic over finite traces is used as a formalism for temporal specification in automated planning, process modelling and (runtime) verification.  In this work, we investigate first-order temporal logic over finite traces, lifting some known results to a more expressive setting. Satisfiability in the two-variable monodic fragment is shown to be ExpSpace-complete, as for the infinite trace case, while it decreases to NExpTime when we consider finite traces bounded in the number of instants. This leads to new complexity results for temporal description logics over finite traces. We further investigate satisfiability and equivalences of formulas under a model-theoretic perspective, providing a set of semantic conditions that characterise when the distinction between reasoning over finite and infinite traces can be blurred.  Finally, we apply these conditions to planning and verification.\n\nAlessandro Artale, Andrea Mazzullo, Ana Ozaki: Do You Need Infinite Time?\nIJCAI 2019: 1516-1522\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=523
LOCATION:Ashton 1.01
END:VEVENT
END:VCALENDAR