主講：李永明教授
報告題目：定量時序邏輯的計算問題
時間：2025年4月24日10:10-12:00
地點：8號教學樓多21教室
主辦單位：數學與計算機應用學院
內容簡介：隨著系統規模的增加，確保系統的安全性和可靠性功能變得愈加重要。模型檢測是一種形式化的自動驗證技術，通過形式化方法發現系統潛在的缺陷，從而及早修正，保障系統的安全性和可靠性。本報告介紹了幾類定量時序邏輯基于決策過程的最優策略模型檢測問題，包含廣義可能性計算樹邏輯（GPoCTL）、廣義可能性線性時序邏輯（GPoLTL）以及可能性多值計算樹邏輯（MvCTL）。證明了系統模型滿足系統性質最優策略的存在性，給出了定量時序邏輯的最優可能性的計算方法，以及對應的最優策略多項式時間的構造方法。此外，介紹一種在可能性模型檢測中基于監督學習的模型量化方法。
歡迎廣大師生前來聆聽交流
報告人簡介：李永明，博士，陜西師范大學二級教授，博士生導師，數學與計算機應用學院客座教授。主要研究方向：邏輯與計算、量子信息學與格上拓撲學。發表高層次論文200余篇，先后主持國家自然科學基金9項、以及973子課題、教育部博士點基金等省部級課題，先后4次獲得教育部科技進步獎、陜西省科學技術獎，獲得第三屆教育部“高校青年教師獎”以及國務院政府津貼等。先后在清華大學、加拿大Alberta大學、澳大利亞悉尼科技大學、德國萊比錫大學、美國肯塔基大學等校訪問和合作研究。（曾）擔任國際IEEE計算智能模糊系統技術委員會委員、中國數學會理事、全國運籌學會智能計算學會副理事長、全國高等師范學校計算機教育委員會副理事長、中國系統工程學會模糊數學與模糊系統委員會副理事長、陜西省考試評價委員會副會長兼高等教育委員會理事長、中國計算機學會理論計算機學會理事等職。曾任多個國際國內會議的大會主席、程序委員會主席、組織委員會主席、委員等，并多次做特邀大會報告。在人才培養方面，多次榮獲國家級教學成果獎、陜西省教學成果獎、校級教學成果獎、省優博論文指導教師獎。
