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 makes them impractical 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\"uchi automaton and an LTL formula respectively. A novel GRL-based framework OCTAL, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification in the latent space. The empirical experiments show that OCTAL achieves comparable accuracy against canonical SOTA model checkers on three different datasets, with up to $5\times$ overall speedup and above $63\times$ for satisfiability checking alone.
Code (0)
등록된 구현이 없습니다.
Tasks
Binary ClassificationGraph Representation LearningmodelRepresentation 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, suffer from the state space explosion problem due to cross …
Binary ClassificationGraph Representation LearningRepresentation 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