主講：李永明教授

報告題目：定量時序邏輯的計算問題

時間：2025年4月24日10:10-12:00

地點：8號教學(xué)樓多21教室

主辦單位：數(shù)學(xué)與計算機應(yīng)用學(xué)院

內(nèi)容簡介：隨著系統(tǒng)規(guī)模的增加，確保系統(tǒng)的安全性和可靠性功能變得愈加重要。模型檢測是一種形式化的自動驗證技術(shù)，通過形式化方法發(fā)現(xiàn)系統(tǒng)潛在的缺陷，從而及早修正，保障系統(tǒng)的安全性和可靠性。本報告介紹了幾類定量時序邏輯基于決策過程的最優(yōu)策略模型檢測問題，包含廣義可能性計算樹邏輯（GPoCTL）、廣義可能性線性時序邏輯（GPoLTL）以及可能性多值計算樹邏輯（MvCTL）。證明了系統(tǒng)模型滿足系統(tǒng)性質(zhì)最優(yōu)策略的存在性，給出了定量時序邏輯的最優(yōu)可能性的計算方法，以及對應(yīng)的最優(yōu)策略多項式時間的構(gòu)造方法。此外，介紹一種在可能性模型檢測中基于監(jiān)督學(xué)習(xí)的模型量化方法。

歡迎廣大師生前來聆聽交流

報告人簡介：李永明，博士，陜西師范大學(xué)二級教授，博士生導(dǎo)師，數(shù)學(xué)與計算機應(yīng)用學(xué)院客座教授。主要研究方向：邏輯與計算、量子信息學(xué)與格上拓?fù)鋵W(xué)。發(fā)表高層次論文200余篇，先后主持國家自然科學(xué)基金9項、以及973子課題、教育部博士點基金等省部級課題，先后4次獲得教育部科技進(jìn)步獎、陜西省科學(xué)技術(shù)獎，獲得第三屆教育部“高校青年教師獎”以及國務(wù)院政府津貼等。先后在清華大學(xué)、加拿大Alberta大學(xué)、澳大利亞悉尼科技大學(xué)、德國萊比錫大學(xué)、美國肯塔基大學(xué)等校訪問和合作研究。（曾）擔(dān)任國際IEEE計算智能模糊系統(tǒng)技術(shù)委員會委員、中國數(shù)學(xué)會理事、全國運籌學(xué)會智能計算學(xué)會副理事長、全國高等師范學(xué)校計算機教育委員會副理事長、中國系統(tǒng)工程學(xué)會模糊數(shù)學(xué)與模糊系統(tǒng)委員會副理事長、陜西省考試評價委員會副會長兼高等教育委員會理事長、中國計算機學(xué)會理論計算機學(xué)會理事等職。曾任多個國際國內(nèi)會議的大會主席、程序委員會主席、組織委員會主席、委員等，并多次做特邀大會報告。在人才培養(yǎng)方面，多次榮獲國家級教學(xué)成果獎、陜西省教學(xué)成果獎、校級教學(xué)成果獎、省優(yōu)博論文指導(dǎo)教師獎。