Quantitative Automata under Probabilistic Semantics

DOI10.1145/2933575.2933588zbMATH Open1401.68155arXiv1604.06764OpenAlexW2342840234MaRDI QIDQ4635863FDOQ4635863

Thomas A. Henzinger, Krishnendu Chatterjee, Jan Otop

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider.

Full work available at URL: https://arxiv.org/abs/1604.06764

zbMATH Keywords

distributionMarkov chainsprobabilityexpected valueweighted automataprobabilistic semanticsnested weighted automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Decidability of theories and sets of sentences (03B25) Semantics in the theory of computing (68Q55)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The complexity of computing the permanent
• Markov Decision Processes with Multiple Objectives
• Markov Decision Processes with Multiple Long-Run Average Objectives
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• Quantitative Multi-objective Verification for Probabilistic Systems
• Discounting in LTL
• Multi-objective Discounted Reward Verification in Graphs and MDPs
• Expressiveness and closure properties for quantitative languages
• Alternating Weighted Automata
• Quantitative languages
• A Survey of Stochastic Games with Limsup and Liminf Objectives
• Weighted Automata and Weighted Logics on Infinite Words
• Temporal Specifications with Accumulative Values
• Quantitative Automata under Probabilistic Semantics
• Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes
• Regular Functions and Cost Register Automata
• Quantitative monitor automata
• Average-energy games
• Non-deterministic Weighted Automata on Random Words
• Pebble Weighted Automata and Transitive Closure Logics
• Trade-off analysis meets probabilistic model checking
• Averaging in LTL
• Weight monitoring with linear temporal logic
• Energy and Mean-Payoff Parity Markov Decision Processes
• Measuring and Synthesizing Systems in Probabilistic Environments
• Nested Weighted Limit-Average Automata of Bounded Width
• Bidirectional nested weighted automata

Cited In (13)

• Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States
• Title not available (Why is that?)
• Non-deterministic weighted automata evaluated over Markov chains
• Monitor Logics for Quantitative Monitor Automata
• Bidirectional nested weighted automata
• Unary probabilistic and quantum automata on promise problems
• Quantitative monitor automata
• Title not available (Why is that?)
• Quantitative Analysis of Randomized Distributed Systems and Probabilistic Automata
• Quantitative Automata under Probabilistic Semantics
• Quantitative Languages Defined by Functional Automata
• Monitoring algorithmic fairness
• Non-deterministic Weighted Automata on Random Words

Uses Software

• PRISM

Recommendations

• Title not available (Why is that?) 👍 👎
• Probabilistic ω-automata 👍 👎
• Approximate Determinization of Quantitative Automata 👍 👎
• Abstract Probabilistic Automata 👍 👎
• Abstract probabilistic automata 👍 👎
• Probabilistic automata of bounded ambiguity 👍 👎
• Quantitative Automata under Probabilistic Semantics 👍 👎
• Probabilistic Automata of Bounded Ambiguity 👍 👎
• Methods for quantitative analysis of probabilistic pushdown automata 👍 👎
• Probabilistic Automata and Probabilistic Logic 👍 👎

This page was built for publication: Quantitative Automata under Probabilistic Semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635863)