主講：李永明教授

報(bào)告題目：定量時(shí)序邏輯的計(jì)算問題

時(shí)間：2025年4月24日10:10-12:00

地點(diǎn)：8號(hào)教學(xué)樓多21教室

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

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

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

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