💻 Category

cs.LO

1112 पेपर

💻 computer science

On the Complexity of Robust Markov Decision Processes and Bisimulation Metrics

यह शोध पत्र पोलिटोपिक अनिश्चितता सेट्स (polytopic uncertainty sets) वाले रोबस्ट मार्कोव डिसीजन प्रोसेस (Robust Markov Decision Processes) की कम्प्यूटेशनल जटिलता की जांच करता है, यह स्थापित करते हुए कि थ्रेशोल्ड समस्या (threshold problem) (s,a)-रेक्टेंगुलर मामलों के लिए NP में और s-रेक्टेंगुलर मामलों के लिए PSPACE में है, जबकि यह सिद्ध करता है कि इसे बहुपद समय (polynomial time) में हल करना इस लंबे समय से चले आ रहे खुले प्रश्न को हल कर देगा कि क्या पैरिटी गेम्स (parity games) P में हैं।

Marnix Suilen, Guillermo A. Pérez2026-04-30
💻 computer science

Runtime Verification: Monitoring, Knowledge, and Uncertainty (Lecture Notes)

ये व्याख्यान नोट्स रनटाइम वेरिफिकेशन (runtime verification) के ऑटोमेटा-सैद्धांतिक (automata-theoretic), टेम्पोरल-लॉजिकल (temporal-logical) और एपिस्टेमिक (epistemic) आधारों को प्रस्तुत करते हैं, जो स्पेसिफिकेशन फॉर्मलिज्म (specification formalisms), डायग्नोसिस (diagnosis), ओपेसिटी (opacity) और मॉनिटेबिलिटी (monitorability) को कवर करते हैं ताकि यह समझाया जा सके कि ऑफलाइन विश्लेषण आंशिक रूप से अवलोकन योग्य प्रणालियों (partially observable systems) के लिए मॉनिटर्स का निर्माण कैसे करता है, जबकि साथ ही रियल-टाइम सेटिंग्स में टाइमेड एक्सटेंशन (timed extensions) की चुनौतियों को भी संबोधित करता है।

Benedikt Bollig2026-04-30
💻 computer science

Full Definability in a Profunctorial Model

यह शोधपत्र स्थापित करता है कि ग्रूपॉइड्स (groupoids) पर आधारित एक प्रूफ-रेलेवेंट रिलेशनल मॉडल में स्थिर (stable) और पूर्ण (total) प्रोफंक्टर्स (profunctors) के सभी लॉजिकल परिवार, MIX के साथ मल्टीप्लिकेटिव लीनियर लॉजिक के प्रूफ-नेट्स द्वारा पूर्णतः परिभाषित हैं, जो यह प्रदर्शित करता है कि इस लक्षण वर्णन के लिए स्थिरता एक महत्वपूर्ण शुद्धता मानदंड के रूप में कार्य करती है।

Takeshi Tsukada, Kazuyuki Asada, Kengo Hirata2026-04-30
💻 computer science

Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

यह शोध पत्र एक एसिंक्रोनस एपिस्टेमिक लॉजिक के लिए एक अनंत स्वयंसिद्ध (infinitary axiomatisation), AA*, प्रस्तावित करता है जो संदेश भेजने और प्राप्त करने के मनमाने इतिहासों का लेखा-जोखा रखता है, जो रिडक्शन सिस्टम दृष्टिकोण और इस धारणा को त्यागकर पूर्व कार्यों का सामान्यीकरण करता है कि कोई भी संदेश प्राप्त नहीं हुआ है।

Philippe Balbiani, Hans van Ditmarsch, Clara Lerouvillois2026-04-29
💻 computer science

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda

यह शोधपत्र क्यूबिकल अगाडा (Cubical Agda) में कौशी वास्तविक संख्याओं (Cauchy real numbers) के होमोटॉपी टाइप थ्योरी (Homotopy Type Theory) निर्माण के औपचारिकीकरण को प्रस्तुत करता है, जो यह प्रदर्शित करता है कि यह दृष्टिकोण अन्य रचनात्मक परिभाषाओं में निहित गणनीय चयन (countable choice), सेटॉइड ओवरहेड (setoid overhead), और यूनिवर्स-स्तर ट्रैकिंग (universe-level tracking) की समस्याओं से बचते हुए बिना पोस्टुलेट्स (postulates) के टाइप-चेक होता है।

Jackson Brough2026-04-29
💻 computer science

Logic of Fuzzy Paths

यह शोधपत्र "लॉजिक ऑफ फजी पाथ्स" (Logic of Fuzzy Paths) को प्रस्तुत करता है, जो मोशन प्लानिंग के लिए एक नया टेम्पोरल लॉजिक है जो ज्यामिति को तर्क से अलग करने के लिए पथों को प्रथम श्रेणी के नागरिक (first-class citizens) के रूप में मानता है, जिससे सिग्नल टेम्पोरल लॉजिक जैसे मौजूदा ढांचों की तुलना में मानव उपयोगकर्ताओं के लिए अधिक सहज विशिष्टताएँ और प्रदर्शन से सीखने की बेहतर क्षमताएँ प्राप्त होती हैं।

Kush Grover, Pratham Gupta, Jan Křetínský2026-04-29
🤖 machine learning

Null Measurability at the Symmetrization Interface in VC Learning

यह शोधपत्र यह प्रदर्शित करता है कि VC लर्निंग के मानक सममितीकरण (symmetrization) प्रमाण में घोस्ट-गैप सुप्रेमा (ghost-gap suprema) के लिए बोरेल मापने योग्यता (Borel measurability) की आवश्यकता जितनी आवश्यक है उससे अधिक है, यह दर्शाते हुए कि इसके बजाय प्रासंगिक बुरी घटनाएँ विश्लेषणात्मक (analytic) हैं और इस प्रकार किसी भी परिमित बोरेल माप के पूर्णता (completion) में मापने योग्य हैं, एक ऐसा परिणाम जिसे Lean 4 में औपचारिक रूप दिया गया है जो PAC लर्नेबिलिटी स्थापित करने के लिए आवश्यक मापने योग्यता की परिकल्पनाओं को कमजोर करता है।

Dhruv Gupta2026-04-29
💻 computer science

Proof Identity and Categorical Models of BV

यह शोध पत्र परमाणु प्रवाह (atomic flows) पर आधारित तर्क BV के लिए प्रमाण पहचान (proof identity) की एक अवधारणा स्थापित करता है और इसका उपयोग BV-श्रेणियों (BV-categories) की परिभाषा को सुदृढ़ करने के लिए करता है, जिससे तर्क के संबंध में उनकी सुसंगतता (soundness) सिद्ध होती है।

Matteo Acclavio, Lutz Straßburger, Vladimir Zamdzhiev2026-04-29
💻 computer science

Partially Finite Model Reasoning in Description Logics Extended Version

यह शोध पत्र परिमित और अनंत तर्क (reasoning) को सामंजस्यपूर्ण बनाने के लिए डिस्क्रिप्शन लॉजिक्स में आंशिक रूप से परिमित मॉडलों (partially finite models) की अवधारणा प्रस्तुत करता है, जो यह सिद्ध करता है कि एक विशिष्ट परिमित अवधारणा वाले लॉजिक S के लिए कंजंक्टिव क्वेरी एंटेलमेंट (conjunctive query entailment) 2-EXPTIME में निर्णायक (decidable) है और क्लोज्ड प्रेडिकेट्स के साथ क्वेरी कंटेनमेंट (query containment) में इसके अनुप्रयोग का प्रदर्शन करता है।

Tomasz Gogacz, Filip Murlak, Marcin Przybyłko, Alexandra Rogova, Michał Skrzypczak2026-04-29
💻 computer science

Positional Properties in Temporal Logic

यह शोध पत्र गेम-आधारित रिएक्टिव सिंथेसिस (game-based reactive synthesis) में पोजीशनल गुणों (positional properties) की जांच करता है, जो लीनियर-टाइम टेम्पोरल लॉजिक (linear-time temporal logic) में उनकी अभिव्यक्तता को प्रदर्शित करता है, पोजीशनलिटी (positionality) के लिए आवश्यक और पर्याप्त स्थितियाँ स्थापित करता है, उनके बूलियन क्लोजर (Boolean closure) पर सीमाओं को सिद्ध करता है, और अल्टरनेटिंग-टाइम टेम्पोरल लॉजिक (alternating-time temporal logic) के सुलभ खंडों (tractable fragments) के लिए उनके निहितार्थों का अन्वेषण करता है।

Jessica Newman, Benjamin Plummer2026-04-29