BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Laura Gamboa Guzmá\;n (Iowa State University) DTSTART:20250501T180000Z DTEND:20250501T190000Z DTSTAMP:20260423T021155Z UID:OLS/178 DESCRIPTION:Title: Fo rmalizing Time: Temporal Logics and the Challenge of Visualizing MLTL\ nby Laura Gamboa Guzmá\;n (Iowa State University) as part of Online logic seminar\n\n\nAbstract\nTemporal logics are a family of modal logics that reason about timelines. They are usually obtained by expanding classi cal propositional logic with modal operators that can qualify the value of a proposition over time\, such as “p will always be true” or “q is true until p becomes true.” However\, different concepts of time are oft en captured by significant logical systems\, as these tend to encode the v arious characteristics that define them\, such as continuous vs. discrete time and linear vs. branching time. The use and development of these logic s have been increasing significantly over the last 50 years\, as researche rs and engineers in fields related to computer science have been using the m to verify safety-critical systems in a formal and precise manner. \n\nIn this talk\, I will introduce some of the better-known temporal logics tha t aim to formalize different concepts of time and briefly explain the diff erent properties that make them good candidates for use in different compu ter-based environments. After that\, I will focus on a logic I have been w orking on during my PhD known as Mission-time (Linear) Temporal Logic (MLT L)\, which is a logic that reasons about finite and discrete timelines (ca lled traces) where finite intervals bound the temporal operators. Although MLTL is only as expressive as classical propositional logic\, it has been capturing the attention of multiple research groups in recent years\, and its succinctness has shown to become a challenge for engineers easily whe n trying to validate the formulas they believe are capturing the desired b ehaviors. For that\, at the Laboratory for Temporal Logic at ISU\, we have been developing algorithms that allow us to take an MLTL formula and prod uce a visual representation for the traces that satisfy the formula.\n LOCATION:https://researchseminars.org/talk/OLS/178/ END:VEVENT END:VCALENDAR