1115 पेपर
Reelay एक एकीकृत, उच्च-प्रदर्शन वाला ऑनलाइन टेम्पोरल लॉजिक मॉनिटरिंग फ्रेमवर्क है जो विविध औपचारिक विनिर्देशों (जैसे LTL, MTL, और STL) को कुशल सिंक्रोनस डेटाफ्लो कंप्यूटेशन ग्राफ में अनुवादित करता है, जिससे विभिन्न हार्डवेयर प्लेटफॉर्म्स पर साइबर-फिजिकल सिस्टम्स के लिए वास्तविक समय में रनटाइम वेरिफिकेशन सक्षम होता है।
यह शोध पत्र एक फजी मोडल लॉजिक (fuzzy modal logic) का परिचय देता है और उसका विश्लेषण करता है जिसे कार्यों और ज्ञान के संबंध में संभाव्य तर्क (probabilistic reasoning) को औपचारिक रूप देने के लिए डिज़ाइन किया गया है, जो कि क्रिपके फ्रेम्स (Kripke frames) पर आधारित एक सिमेंटिक फ्रेमवर्क प्रदान करता है और इसके संतुष्टि समस्याओं (satisfiability problems) की कम्प्यूटेशनल जटिलता को निर्धारित करता है।
यह शोध पत्र उन ग्राफ वर्गों की जांच और लक्षण वर्णन करता है जिनके लिए प्रथम-क्रम मॉडल चेकिंग समस्या (first-order model checking problem) सूत्र में चरों की संख्या द्वारा पैरामीटराइज्ड होने पर एक FPT-समय एल्गोरिदम स्वीकार करती है, विशेष रूप से मोनोटोन और हेरेडिटरी सेटिंग्स में लक्षण वर्णन प्रदान करते हुए।
DEKL 2.0 एक आश्रित प्रकार-सैद्धांतिक (dependent type-theoretic) ढांचा है जो ज्ञान को एक ट्रेस श्रेणी (trace category) पर एक प्रीशीफ (presheaf) के रूप में मॉडल करके निष्पादन योग्य ट्रेस (executable traces) और ज्ञान संशोधन को एकीकृत करता है, जिससे एक मोनोटोनिक प्रमाण पंचांग (monotone proof calculus) को बनाए रखते हुए गैर-मोनोटोनिक विकास (non-monotonic evolution) अर्थपूर्ण रूप से उभरता है।
यह शोध पत्र सिद्ध करता है कि एपिस्टेमिक लॉजिक (epistemic logic) में प्लान अस्तित्व समस्या (plan existence problem) अनिर्णयक्षम (undecidable) है, यहाँ तक कि अत्यधिक प्रतिबंधित स्थितियों के तहत भी जैसे कि एक्शन प्रीकंडिशन्स (action preconditions) के लिए सीमित मोडल डेप्थ (modal depth) और पोस्टकंडिशन्स (postconditions) की अनुपस्थिति।
यह शोध पत्र एक एकीकृत औपचारिक ढांचे को प्रस्तुत करके रिकर्सिव (recursive) ShEx और SHACL स्कीमा भाषाओं के बीच अर्थ संबंधी विचलन (semantic divergence) को संबोधित करता है जो लीस्ट (least) और ग्रेटेस्ट (greatest) फिक्स्पॉइंट सिमेंटिक्स के बीच संबंधों को स्पष्ट करता है, दोनों मानकों के बीच अभिव्यंजक रूप से समकक्ष अंशों (expressively equivalent fragments) के अस्तित्व को प्रदर्शित करता है, और उनके संबंधित कम्प्यूटेशनल जटिलताओं का विश्लेषण करता है।
यह शोधपत्र VerCors-relaxed प्रस्तुत करता है, जो VerCors डीडक्टिव वेरिफिकेशन टूल का एक विस्तार है, जो व्यू-आधारित प्रोटोकॉल और परमिशन-आधारित सेपरेशन लॉजिक का उपयोग करके वीक मेमोरी कंकरेंसी को एनकोड करता है ताकि उन कंकरेंट प्रोग्राम्स के स्वचालित सत्यापन को सक्षम बनाया जा सके जो पहले मैनुअल प्रूफ तक ही सीमित थे।
यह शोध पत्र पारेटो (Pareto), वैश्विक (global) और पूर्णता-इष्टतम (completion-optimal) सुधारों का उपयोग करके प्राथमिकता वाले डेटा की विसंगति-सहनशील पूछताछ के लिए एक ASP(Q)-आधारित ढांचे को प्रस्तुत और कार्यान्वित करता है, जो उनके कम्प्यूटेशनल जटिलता और व्यावहारिक व्यवहार्यता का विश्लेषण करते हुए वैश्विक-इष्टतम और ग्राउंडेड अर्थों (grounded semantics) के लिए पहले सिस्टम प्रदान करता है।
यह शोध पत्र A-IC3 का प्रस्ताव करता है, जो एक हल्का मशीन-लर्निंग फ्रेमवर्क है जो IC3 हार्डवेयर मॉडल चेकिंग एल्गोरिदम के लिए इष्टतम इंडक्टिव जनरलाइजेशन रणनीतियों को गतिशील रूप से चुनने के लिए एक मल्टी-आर्म्ड बैंडिट एल्गोरिदम का उपयोग करता है, जिससे एक बड़े बेंचमार्क सुइट पर इसके प्रदर्शन और स्केलेबिलिटी में महत्वपूर्ण सुधार होता है।
यह शोध पत्र सुरक्षा प्रोटोकॉल विश्लेषण में निर्णीय (decidable) ज्ञान समस्याओं के दायरे को विस्तृत करने के लिए ग्राफ-एम्बेडेड टर्म रीराइट सिस्टम्स को प्रस्तुत करता है, जो संकुचित अभिसारी (contracting convergent) उपवर्ग के लिए निर्णीयता सिद्ध करते हुए व्यापक वर्ग के लिए अनिर्णीयता प्रदर्शित करता है, और साथ ही अन्य समीकरण सिद्धांतों (equational theories) के साथ संयोजन परिणाम भी प्रदान करता है।