Academic publications on bounded model checking, multi-agent systems, and formal verification by the NextBMC Platform research team.
32 papers found
Presents an SMT-based bounded model checking approach for dense-timed deontic interpreted systems, enabling formal verification of multi-agent systems with obligations, permissions, and real-time constraints.
Proposes an improved spatial hashing algorithm with linear memory footprint and parallelism support, targeting performance-critical state-space lookup in agent-based simulations.
Develops an SMT-based BMC procedure for verifying EMTLK (Epistemic Metric Temporal Logic with Knowledge) properties over dense-timed interpreted systems used in multi-agent reasoning.
Investigates extrapolation of optimal agent policies in multi-agent systems using statistical probabilistic model checking, combining simulation-based techniques with formal guarantees.
Introduces a real-time extension of commitment logic for multi-agent systems, combining temporal duration constraints with inter-agent communication modeled as interpreted systems.
Applies formal verification techniques to model and check robustness properties of communication protocols among autonomous vehicle agents.
Proposes an SMT-based method for finding k-quasi-optimal runs in weighted timed automata, with applications to planning and near-optimal scheduling in real-time systems.
Presents a complete BMC-based framework for verifying Epistemic Metric Temporal Logic with Knowledge (EMTLK) properties in timed multi-agent interpreted systems via a SAT-based encoding.
Extends deontic interpreted systems with quantitative weights and introduces a SAT-based BMC procedure to verify normative and epistemic properties subject to cost constraints.
Presents a GPU-accelerated simulator for the PRISM probabilistic model checker, enabling high-throughput statistical verification of probabilistic concurrent systems.
Workshop version of the optimal policy extrapolation work via statistical probabilistic model checking; extended into the Fundamenta Informaticae journal paper (2018).
Introduces SMT-based BMC for the weighted epistemic extension of CTL (ECTL), enabling verification of multi-agent systems with quantitative cost and knowledge operators.
Conference presentation combining weighted interpreted systems with SMT-based BMC for weighted epistemic ECTL in multi-agent environments.
Doctoral consortium overview of SAT- and SMT-based model checking methods for verifying properties of multi-agent systems and timed interpreted systems.
Workshop paper on SMT-based search for k-quasi-optimal execution runs in weighted timed automata, bridging optimization and formal verification for real-time agent systems.
Comprehensive empirical and theoretical comparison of BDD-based and SAT-based BMC for verifying the existential fragment of LTL extended with epistemic knowledge operators in multi-agent systems.
Extends interpreted systems with quantitative weights and introduces a BMC procedure for the flat fragment of weighted epistemic CTL, enabling cost-aware agent system verification.
Conference presentation of a BMC approach for checking EMTLK properties of timed interpreted systems — the formal model for multi-agent knowledge reasoning with metric time.
Introduces a BMC procedure for verifying Metric Temporal Logic (MTL) properties over discrete timed automata, providing an effective SAT-based falsification technique for real-time systems.
Extended abstract introducing SAT-based BMC for deontic interpreted systems with quantitative weights representing costs of norm violations in multi-agent environments.
Proposes a translation from Metric Interval Temporal Logic (MITL) to a fragment of Hybrid LTL, enabling the use of existing SAT/BMC tools for real-time existential model checking.
Workshop version of the MTL-over-discrete-timed-automata BMC work; precursor to the Fundamenta Informaticae journal paper (2014).
Presents a SAT-based BMC approach for the existential fragment of LTL applied to multi-agent system reachability and safety properties.
Introduces BMC for epistemic extensions of CTL, allowing agents' knowledge and beliefs to be incorporated directly into branching-time model checking.
Develops a SAT-based BMC procedure targeting interpreted systems — the standard formal model for reasoning about multi-agent knowledge and epistemic properties.
One of the early works applying bounded model checking to multi-agent systems modeled as interpreted systems, exploring both SAT and BDD-based encodings.
Extends bounded model checking to diagonal timed automata — a richer class than standard timed automata — enabling more expressive real-time system verification with SAT-based tools.
Artificial Intelligence journal version presenting comprehensive foundations and proofs for the SAT-based BMC approach for diagonal timed automata.
Applies bounded model checking to verify the TESLA broadcast authentication protocol in a multi-agent context, demonstrating BMC's applicability to security protocol analysis.
Presents both the theoretical foundations and practical implementation aspects of bounded model checking, covering SAT-based encodings for temporal and epistemic logics.
Establishes completeness and decidability results for bounded model checking, providing theoretical guarantees for SAT-based falsification of temporal logic properties in agent systems.
Foundational work applying bounded model checking to real-time systems modeled with timed automata, establishing the SAT-based approach for timed reachability verification.