1115 पेपर
यह शोध पत्र GORED का प्रस्ताव करता है, जो एक सामान्य अनुकूलन सॉल्वर (optimization solver) है जो विविध अनुकूलन समस्याओं को स्वचालित रूप से MaxSAT उदाहरणों में कम करके समस्या-समाधान बहुमुखीता को बढ़ाता है, जिससे एक एकल एकीकृत ढांचा विशिष्ट एल्गोरिदम के तुलनीय समाधान गुणवत्ता प्राप्त करने में सक्षम होता है।
यह शोधपत्र "प्रायिकतात्मक अपोहन" (probabilistic abduction) की जटिलता को औपचारिक रूप देने और अध्ययन करने के लिए एक फजी प्रायिक तर्क () प्रस्तुत करता है, जो कि घटनाओं की प्रायिकता के बारे में दिए गए प्रेक्षणों से तार्किक रूप से निहित होने वाले प्रायिकता वितरणों या कथनों को खोजने की एक प्रक्रिया है।
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) के लिए पहले सिस्टम प्रदान करता है।