Pages that link to "Item:Q1193587"
From MaRDI portal
The following pages link to Symbolic model checking: \(10^{20}\) states and beyond (Q1193587):
Displayed 50 items.
- On the expressivity and complexity of quantitative branching-time temporal logics (Q1401306) (← links)
- Well-abstracted transition systems: Application to FIFO automata. (Q1401924) (← links)
- A satisfiability procedure for quantified Boolean formulae (Q1408385) (← links)
- Binary decision diagrams for first-order predicate logic. (Q1426055) (← links)
- Symbolic state-space exploration and numerical analysis of state-sharing composed models (Q1434418) (← links)
- Symbolic model checking for \(\mu\)-calculus requires exponential time (Q1575656) (← links)
- Stochastic dynamic programming with factored representations (Q1583230) (← links)
- Randomized OBDD-based graph algorithms (Q1625606) (← links)
- Practical verification of multi-agent systems against \textsc{Slk} specifications (Q1641030) (← links)
- Symbolic perimeter abstraction heuristics for cost-optimal planning (Q1647507) (← links)
- An explicit transition system construction approach to LTL satisfiability checking (Q1707341) (← links)
- Model checking properties on reduced trace systems (Q1736621) (← links)
- Hybrid and subexponential linear logics (Q1744445) (← links)
- The complexity of counting models of linear-time temporal logic (Q1745344) (← links)
- Structuring and automating hardware proofs in a higher-order theorem- proving environment (Q1801500) (← links)
- Decidable integration graphs. (Q1854273) (← links)
- Specification in CTL + past for verification in CTL. (Q1854327) (← links)
- Iterating transducers (Q1858440) (← links)
- Syntax-directed model checking of sequential programs (Q1858441) (← links)
- Symbolic synthesis of masking fault-tolerant distributed programs (Q1938357) (← links)
- Exponential improvement of time complexity of model checking for multiagent systems with perfect recall (Q1938921) (← links)
- Formal verification based on Boolean expression diagrams (Q1954165) (← links)
- Discrete-time control for rectangular hybrid automata (Q1960531) (← links)
- Compositional reasoning for shared-variable concurrent programs (Q2024370) (← links)
- On the number of active states in finite automata (Q2041683) (← links)
- Generating extended resolution proofs with a BDD-based SAT solver (Q2044191) (← links)
- Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models (Q2095426) (← links)
- Lazy regular sensing (Q2112190) (← links)
- Improving the filtering of branch-and-bound MDD solver (Q2117223) (← links)
- Automata-driven partial order reduction and guided search for LTL model checking (Q2152647) (← links)
- Offline and online monitoring of scattered uncertain logs using uncertain linear dynamical systems (Q2165213) (← links)
- First-order temporal logic monitoring with BDDs (Q2225472) (← links)
- Static analysis and stochastic search for reachability problem (Q2229143) (← links)
- Symbolic coloured SCC decomposition (Q2233494) (← links)
- Verification and enforcement of access control policies (Q2248087) (← links)
- Approximate verification of strategic abilities under imperfect information (Q2289016) (← links)
- Two AGM-style characterizations of model repair (Q2294584) (← links)
- An automata-theoretic approach to model-checking systems and specifications over infinite data domains (Q2331081) (← links)
- Counterexample-preserving reduction for symbolic model checking (Q2336646) (← links)
- Terminal satisfiability in GSTE (Q2336669) (← links)
- The complexity of automated addition of fault-tolerance without explicit legitimate states (Q2355327) (← links)
- On the universal and existential fragments of the \(\mu\)-calculus (Q2368950) (← links)
- Bounded model checking of infinite state systems (Q2369883) (← links)
- Verification of SpecC using predicate abstraction (Q2369884) (← links)
- Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams (Q2372185) (← links)
- Symbolic model checking for probabilistic timed automata (Q2373877) (← links)
- GSTE is partitioned model checking (Q2385196) (← links)
- On the number of active states in deterministic and nondeterministic finite automata (Q2399248) (← links)
- Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes (Q2407982) (← links)
- Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving (Q2418047) (← links)