Σεμινάριο Θεωρητικής Πληροφορικής – Τυπικών Μεθόδων
Πέμπτη 21 Μαΐου ώρα 12:00, Αίθουσα M2
“Towards verifying quantitative properties with weighted LTL”
Dr Ελένη Μανδραλή (https://st.ihu.gr/posts/post-profiles/eleni-mandrali)
Μεταδιδακτορική ερευνήτρια
Διεθνές Πανεπιστήμιο Ελλάδας
Linear Temporal Logic (LTL) was proposed by Pnueli as a specification language that can be used in verifying qualitative properties of complex systems, and it has been used successfully in industrial verification tools that aim to verify that a system’s behavior is correct with respect to a desired property. Due to the complexity of modern systems there is an increasing need to expand the verification goals to quantitative aspects of a system’s behavior.
In this talk, we present a weighted Linear Temporal Logic with weights over (ω,≤)-valuation monoids and focus on examples of its ability to specify properties of quantitative bahaviors. We present the definition of syntactic fragments of the logic whose formulas’ semantics express a notion of weighted safety, and a decision procedure that given a formula in these fragments and a weighted Buchi automaton decides whether the behavior of the automaton coincides with the semantics of the formula.
https://grahonis.webpages.auth.gr/Seminar_TCS-FM.html
Οι υπεύθυνοι του σεμιναρίου
καθ. Παναγιώτης Κατσαρός (τμήμα Πληροφορικής)
καθ. Γεώργιος Ραχώνης