Develops polynomial-time PMC for FDFA and introduces FUFA for succinct ω-regular specs with improved LTL translation.
hub
18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977 , pages =
22 Pith papers cite this work. Polarity classification is still indexing.
22
Pith papers citing it
hub tools
citation-role summary
background 3
citation-polarity summary
roles
background 3polarities
background 3representative citing papers
A meta-programming framework operationalizes TEL, MEL, and DEL semantics in ASP via clingo grammar extensions, type specifications, nesting, and a grounding protection pipeline, demonstrated through the metasp system.
TraceFix repairs LLM-generated multi-agent protocols via TLA+ counterexamples to achieve full verification on all tested tasks and higher completion rates than prompt-only baselines.
AIC is a new equational algebra for deriving fixed points from iterations that proves the Tarski-Kantorovich principle, a k-induction generalization, and a novel limit-inf/sup theorem, with Isabelle mechanization and completeness analysis.
Local attention in fixed-precision transformers introduces a second past operator in linear temporal logic, strictly increasing expressivity over global attention alone, with hybrids being most expressive.
SafeDec uses constrained decoding to ensure autoregressive robot navigation foundation models generate actions that provably satisfy STL safety specifications under assumed dynamics.
Tool-using LLM agents can implement undetectable stegosystems, shifting the primary barrier to covert multi-agent collusion from technical feasibility to coordination without explicit agreement.
A neuro-symbolic framework compiles LTLf formulas to DFAs, derives differentiable satisfaction signals from DFA progression, and uses them as a logic-based regularization loss to enforce temporal constraints in autoregressive transformer RL policies while preserving competitive returns.
The paper establishes syntactic correspondences between non-wellfounded and cyclic proofs for LTL in linear nested sequents by proving completeness relative to saturation recurrence and introducing an unraveling shift procedure.
The authors introduce a three-part ontology-based verification system for AI agents that generates regulatory and adversarial test scenarios and issues machine-verifiable trust certificates, with pilot results indicating improved coverage over baselines in four industries.
Combines LTL formal methods with LLMs for auditing, predictive monitoring, and runtime intervention on temporally extended behavioral constraints, outperforming LLM baselines and reducing violations.
A neuro-symbolic system using large reasoning models and model checkers outperforms dedicated reactive synthesis tools on benchmarks and handles parameterized systems.
ClarifySTL uses LLM agents to interactively detect and resolve vagueness and ambiguity in natural language requirements via clarification queries before generating STL formulas, with evaluations on existing and new benchmarks showing effectiveness.
A formal model of minimal evidence for each CTL operator is defined and paired with an implemented visualization scheme for witnesses and counterexamples.
Develops cyclic labelled sequent calculi for propositional and first-order process logic over regular programs, with soundness via infinite descent and completeness via derivation of prior rules.
Presents a Tseitin-like translation reducing arbitrary metric temporal formulas to past-operator logic programs under answer set semantics for use with ASP solvers.
Provides complexity results for the constrained existence problem of five equilibrium notions in multiplayer graph games.
SemML 2.0 outperforms prior LTL synthesis tools on SYNTCOMP by solving more instances faster with comparable solution quality.
TREBL is a sound and relatively complete temporal logic fragment for expressing and proving liveness conditions in Event-B machines under sufficient refinement.
LLMs handle LTL syntax better than semantics, improve with detailed prompts, and perform substantially better when the task is reframed as Python code completion.
Case study shows that SPIN and DIVINE model checkers can uncover design flaws and code defects in a C++ framework missed by hundreds of hours of testing and can be integrated into the development workflow.
A survey that maps risks along the agent workflow and consolidates metrics and benchmarks for safety, robustness, privacy, and security in agentic AI.
citing papers explorer
-
Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata
Develops polynomial-time PMC for FDFA and introduces FUFA for succinct ω-regular specs with improved LTL translation.
-
Meta-Programming for Linear-time Temporal Answer Set Programming
A meta-programming framework operationalizes TEL, MEL, and DEL semantics in ASP via clingo grammar extensions, type specifications, nesting, and a grounding protection pipeline, demonstrated through the metasp system.
-
TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples
TraceFix repairs LLM-generated multi-agent protocols via TLA+ counterexamples to achieve full verification on all tested tasks and higher completion rates than prompt-only baselines.
-
The Algebra of Iterative Constructions
AIC is a new equational algebra for deriving fixed points from iterations that proves the Tarski-Kantorovich principle, a k-induction generalization, and a novel limit-inf/sup theorem, with Isabelle mechanization and completeness analysis.
-
Characterizing the Expressivity of Local Attention in Transformers
Local attention in fixed-precision transformers introduces a second past operator in linear temporal logic, strictly increasing expressivity over global attention alone, with hybrids being most expressive.
-
Constrained Decoding for Safe Robot Navigation Foundation Models
SafeDec uses constrained decoding to ensure autoregressive robot navigation foundation models generate actions that provably satisfy STL safety specifications under assumed dynamics.
-
Tool Use Enables Undetectable Steganography in Multi-Agent LLM Systems
Tool-using LLM agents can implement undetectable stegosystems, shifting the primary barrier to covert multi-agent collusion from technical feasibility to coordination without explicit agreement.
-
Neuro-Symbolic Injection of LTLf Constraints in Autoregressive Reinforcement Learning Policies
A neuro-symbolic framework compiles LTLf formulas to DFAs, derives differentiable satisfaction signals from DFA progression, and uses them as a logic-based regularization loss to enforce temporal constraints in autoregressive transformer RL policies while preserving competitive returns.
-
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
The paper establishes syntactic correspondences between non-wellfounded and cyclic proofs for LTL in linear nested sequents by proving completeness relative to saturation recurrence and introducing an unraveling shift procedure.
-
Toward Pre-Deployment Assurance for Enterprise AI Agents: Ontology-Grounded Simulation and Trust Certification
The authors introduce a three-part ontology-based verification system for AI agents that generates regulatory and adversarial test scenarios and issues machine-verifiable trust certificates, with pilot results indicating improved coverage over baselines in four industries.
-
Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems
Combines LTL formal methods with LLMs for auditing, predictive monitoring, and runtime intervention on temporally extended behavioral constraints, outperforming LLM baselines and reducing violations.
-
Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
A neuro-symbolic system using large reasoning models and model checkers outperforms dedicated reactive synthesis tools on benchmarks and handles parameterized systems.
-
ClarifySTL: An Interactive LLM Agent Framework for STL Transformation through Requirements Clarification
ClarifySTL uses LLM agents to interactively detect and resolve vagueness and ambiguity in natural language requirements via clarification queries before generating STL formulas, with evaluations on existing and new benchmarks showing effectiveness.
-
Visualising CTL Witnesses and Counterexamples -- Extended Version
A formal model of minimal evidence for each CTL operator is defined and paired with an implemented visualization scheme for witnesses and counterexamples.
-
Labelled Process Logic
Develops cyclic labelled sequent calculi for propositional and first-order process logic over regular programs, with soundness via infinite descent and completeness via derivation of prior rules.
-
Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics
Presents a Tseitin-like translation reducing arbitrary metric temporal formulas to past-operator logic programs under answer set semantics for use with ASP solvers.
-
Equilibria in Multiplayer Graph Games: An Algorithmic Study
Provides complexity results for the constrained existence problem of five equilibrium notions in multiplayer graph games.
-
SemML 2.0: Synthesizing Controllers for LTL
SemML 2.0 outperforms prior LTL synthesis tools on SYNTCOMP by solving more instances faster with comparable solution quality.
-
TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory
TREBL is a sound and relatively complete temporal logic fragment for expressing and proving liveness conditions in Event-B machines under sufficient refinement.
-
Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation
LLMs handle LTL syntax better than semantics, improve with detailed prompts, and perform substantially better when the task is reframed as Python code completion.
-
Model Checking a C++ Software Framework, a Case Study
Case study shows that SPIN and DIVINE model checkers can uncover design flaws and code defects in a C++ framework missed by hundreds of hours of testing and can be integrated into the development workflow.
-
Towards trustworthy agentic AI: a comprehensive survey of safety, robustness, privacy, and system security
A survey that maps risks along the agent workflow and consolidates metrics and benchmarks for safety, robustness, privacy, and security in agentic AI.