OCTAL: Graph Representation Learning for LTL Model Checking
Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, suffer from the state space explosion problem due to cross product operations required that make them prohibitively expensive for large-scale systems and/or specifications. In this paper, we propose to use graph representation learning (GRL) for solving linear temporal logic (LTL) model checking, where the system and the specification are expressed by a B{\"u}chi automaton and an LTL formula, respectively. A novel GRL-based framework \model, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification. Empirical experiments on two model checking scenarios show that \model achieves promising accuracy, with up to $11\times$ overall speedup against canonical SOTA model checkers and $31\times$ for satisfiability checking alone.
Code (0)
등록된 구현이 없습니다.
Tasks
Binary ClassificationGraph Representation LearningRepresentation LearningSimilar Papers 제목 키워드 기반
OCTAL: Graph Representation Learning for LTL Model Checking
Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, still suffer from the state space explosion problem that ma…
Binary ClassificationGraph Representation LearningmodelRepresentation LearningDocTalk: Scalable Graph-based Dialogue Synthesis for Enhancing LLM Conversational Capabilities
Large Language Models (LLMs) are increasingly employed in multi-turn conversational tasks, yet their pre-training data predominantly consists of continuous prose, creating a potential mismatch between required capabiliti…
DocTalkBN: A Novel Dataset of Expert Telemedicine Conversations in Bengali
Reliable medical conversational AI requires authentic expert--patient interaction data, yet such datasets remain scarce, especially for low-resource languages such as Bengali. We present DocTalkBN, a large-scale multimod…
Medical Named Entity RecognitionA Novel Octal Annular Ring-Shaped Planar Monopole Antenna For WiFi And Unlicensed Ultra Wideband Frequency Range Applications
Our paper presents the design of a unique annular ring-shaped planar monopole antenna with octal geometry intended for a broad spectrum of frequency applications. Utilizing FR4 epoxy for the substrate and copper material…
Online Low Rank Matrix Completion
We study the problem of {\em online} low-rank matrix completion with $\mathsf{M}$ users, $\mathsf{N}$ items and $\mathsf{T}$ rounds. In each round, the algorithm recommends one item per user, for which it gets a (noisy) …
ClusteringCollaborative FilteringLow-Rank Matrix CompletionMatrix Completion