主講：李永明教授

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

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

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

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

內(nèi)容簡(jiǎn)介：隨著系統(tǒng)規(guī)模的增加，確保系統(tǒng)的安全性和可靠性功能變得愈加重要。模型檢測(cè)是一種形式化的自動(dòng)驗(yàn)證技術(shù)，通過(guò)形式化方法發(fā)現(xiàn)系統(tǒng)潛在的缺陷，從而及早修正，保障系統(tǒng)的安全性和可靠性。本報(bào)告介紹了幾類定量時(shí)序邏輯基于決策過(guò)程的最優(yōu)策略模型檢測(cè)問(wèn)題，包含廣義可能性計(jì)算樹(shù)邏輯（GPoCTL）、廣義可能性線性時(shí)序邏輯（GPoLTL）以及可能性多值計(jì)算樹(shù)邏輯（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í)的模型量化方法。

歡迎廣大師生前來(lái)聆聽(tīng)交流

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