scientific article; zbMATH DE number 4124989
From MaRDI portal
Publication:4205072
zbMath0686.68015MaRDI QIDQ4205072
Publication date: 1989
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
program specificationtemporal logicconcurrencyprogram derivationasynchronous reactive programprogram synthesis by constructive theorem proving
Analysis of algorithms and problem complexity (68Q25) Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Related Items (only showing first 100 items - show all)
Reactive synthesis from visibly register pushdown automata ⋮ Equilibria for games with combined qualitative and quantitative objectives ⋮ Adapting behaviors via reactive synthesis ⋮ Modular strategies for recursive game graphs ⋮ The computational complexity of scenario-based agent verification and design ⋮ Distributed synthesis for well-connected architectures ⋮ Verifying specifications in the language L against temporal properties nonexpressible in this language ⋮ Synthesis with rational environments ⋮ Imperfect information in reactive modules games ⋮ Linear temporal logic -- from infinite to finite horizon ⋮ Determinization and limit-determinization of Emerson-Lei automata ⋮ Incorporating monitors in reactive synthesis without paying the price ⋮ On control of systems modelled as deterministic Rabin automata ⋮ Maintenance goals of agents in a dynamic environment: formulation and policy construction ⋮ MetateM: An introduction ⋮ Supervision based on place invariants: a survey ⋮ A transformation-based synthesis of temporal specification ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ Planning for potential: efficient safe reinforcement learning ⋮ The synthesis problem for repeatedly communicating Petri games ⋮ From model checking to equilibrium checking: reactive modules for rational verification ⋮ Safraless LTL synthesis considering maximal realizability ⋮ A theory of formal synthesis via inductive learning ⋮ On the relation between reactive synthesis and supervisory control of non-terminating processes ⋮ Latticed-LTL synthesis in the presence of noisy inputs ⋮ Control of \(\omega\)-automata under state fairness assumptions ⋮ Mean-payoff games with \(\omega\)-regular specifications ⋮ Parameterized linear temporal logics meet costs: still not costlier than LTL ⋮ Finite-state strategies in delay games ⋮ Optimal bounds in parametric LTL games ⋮ Connectivity games over dynamic networks ⋮ Robust, expressive, and quantitative linear temporal logics: pick any two for free ⋮ Planning control rules for reactive agents ⋮ Information tracking in games on graphs ⋮ Finite automata on timed \(\omega\)-trees ⋮ Simulation relations for fault-tolerance ⋮ Infinite-duration poorman-bidding games ⋮ Symbolic synthesis of masking fault-tolerant distributed programs ⋮ Profile trees for Büchi word automata, with application to determinization ⋮ Supervisory control and reactive synthesis: a comparative introduction ⋮ Augmented finite transition systems as abstractions for control synthesis ⋮ Finding and fixing faults ⋮ Coping with selfish on-going behaviors ⋮ Synthesizing bounded-time 2-phase fault recovery ⋮ Harmonization of interacting automata ⋮ On computability of data word functions defined by transducers ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Moving in a network under random failures: a complexity analysis ⋮ Symbolic supervisory control of infinite transition systems under partial observation using abstract interpretation ⋮ Complexity of synthesis of composite service with correctness guarantee ⋮ Reliability-aware automatic composition approach for web services ⋮ Synthesis of Reactive(1) designs ⋮ Efficiently solving quantified bit-vector formulas ⋮ Antichains and compositional algorithms for LTL synthesis ⋮ Symbolic bounded synthesis ⋮ Automation of fault-tolerant graceful degradation ⋮ Indecision and delays are the parents of failure -- taming them algorithmically by synthesizing delay-resilient control ⋮ Simple stochastic games with almost-sure energy-parity objectives are in NP and conp ⋮ Concurrent reachability games ⋮ GR(1)*: GR(1) specifications extended with existential guarantees ⋮ Computable concurrent processes ⋮ Maximally permissive controlled system synthesis for non-determinism and modal logic ⋮ Problems of synthesis of \(\Sigma\)-automata specified in languages LP and LF of first order logic ⋮ Parametric linear dynamic logic ⋮ Reactive synthesis without regret ⋮ On undecidability of propositional temporal logics on trace systems ⋮ Strategy synthesis for multi-dimensional quantitative objectives ⋮ Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\) ⋮ Synthesizing robust systems ⋮ On subgame perfect equilibria in turn-based reachability timed games ⋮ Energy parity games ⋮ Mechanising first-order temporal resolution ⋮ Conversation protocols: a formalism for specification and verification of reactive electronic services ⋮ Automata-based axiom pinpointing ⋮ Strategy logic ⋮ The complexity of agent design problems: Determinism and history dependence ⋮ CTL\(^\ast\) with graded path modalities ⋮ Refutation-based synthesis in SMT ⋮ Synthesizing adaptive test strategies from temporal logic specifications ⋮ Assume-guarantee synthesis for digital contract signing ⋮ Program repair without regret ⋮ Practical synthesis of reactive systems from LTL specifications via parity games ⋮ Performance heuristics for GR(1) synthesis and related algorithms ⋮ A symbolic algorithm for lazy synthesis of eager strategies ⋮ Synthesis from hyperproperties ⋮ Safety synthesis for incrementally stable switched systems using discretization-free multi-resolution abstractions ⋮ Vacuity in synthesis ⋮ Automata on infinite trees ⋮ From liveness to promptness ⋮ A verification-driven framework for iterative design of controllers ⋮ Relating word and tree automata ⋮ Module checking ⋮ On-the-fly informed search of non-blocking directed controllers ⋮ Iterated Boolean games ⋮ A model of concurrency with fair merge and full recursion ⋮ Compositional construction of most general controllers ⋮ Proving partial order properties ⋮ Weak, strong, and strong cyclic planning via symbolic model checking ⋮ The complexity of automated addition of fault-tolerance without explicit legitimate states ⋮ Back to the future: a fresh look at linear temporal logic
This page was built for publication:
