NDLI: Trade-off analysis meets probabilistic model checking

Please wait, while we are loading the content...

Trade-off analysis meets probabilistic model checking

Understanding biology through logic

The Ackermann award 2014

Infinite-state energy games

Abstract interpretation: past, present and future

Computer-checked mathematics: a formal proof of the odd order theorem

Citations for the test-of-time award from 1994

Beta reduction is invariant, indeed

Regular combinators for string transformations

Asymptotic behaviour in temporal logic

Weight monitoring with linear temporal logic: complexity and decidability

Graph logics with rational relations: the role of word combinatorics

Effective interpolation and preservation in guarded logics

On the discriminating power of passivation and higher-order interaction

A domain-theoretic approach to Brownian motion and general continuous stochastic processes

Two-way cost automata and cost logics over infinite trees

Decomposition theorems and model-checking for the modal μ-calculus

Logic for communicating automata with parameterized topology

Logical characterization of weighted pebble walking automata

Coinduction up-to in a fibrational setting

Model checking existential logic on partially ordered sets

Zero-reachability in probabilistic multi-counter automata

The complexity of admissibility in Omega-regular games

On the characterization of models of H

A decision procedure for satisfiability in separation logic with inductive predicates

Secure equilibria in weighted games

Weak MSO: automata and expressiveness modulo bisimilarity

Symmetry in concurrent games

Decidability of weak logics with deterministic transitive closure

Equality and fixpoints in the calculus of structures

The tractability frontier of graph-like first-order query sets

One hierarchy spawns another: graph deconstructions and the complexity classification of conjunctive queries

On the total variation distance of labelled Markov chains

System F with coercion constraints

The geometry of synchronization

On the pigeonhole and related principles in deep inference and monotone systems

Expressive completeness of separation logic with two variables and no separating conjunction

A new correctness criterion for MLL proof nets

On periodically iterated morphisms

Pattern logics and auxiliary relations

Substitution, jumps, and algebraic effects

Satisfiability modulo counting: a new approach for analyzing privacy properties

Achieving new upper bounds for the hypergraph duality problem through logic

Symmetric normalisation for intuitionistic logic

Equilibria of concurrent games on event structures

Subclasses of presburger arithmetic and the weak EXP hierarchy

Senescent ground tree rewrite systems

Preservation and decomposition theorems for bounded degree structures

No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete

Abstract interpretation from Büchi automata

Memoryful geometry of interaction: from coalgebraic components to algebraic effects

Axioms and decidability for type isomorphism in the presence of sums

Functional reactive types

Probably safe or live

A quest for algorithmically random infinite structures

On the succinctness of query rewriting over shallow ontologies

Turing machines with atoms, constraint satisfaction problems, and descriptive complexity

Local temporal reasoning

On Hanf-equivalence and the number of embeddings of small induced subgraphs

Non-elementary complexities for branching VASS, MELL, and extensions

Infinite sequential games with real-valued payoffs

Hyper-Ackermannian bounds for pushdown vector addition systems

Transition systems over games

Compositional verification of termination-preserving refinement of concurrent programs

Eilenberg-MacLane spaces in homotopy type theory

MSO queries on trees: enumerating answers under updates

On the computing power of +, -, and ×

On the Hoare theory of monadic recursion schemes

Formulae-as-types for an involutive negation

A type theory for productive coprogramming via guarded recursion

Deadlock and lock freedom in the linear π-calculus

On context semantics and interaction nets

Anchored LTL separation

Separating regular languages with first-order logic

Logics with counting and equivalence

A functional functional interpretation

Compositional higher-order model checking via ω-regular games over Böhm trees

Finite-memory strategy synthesis for robust multidimensional mean-payoff objectives

Faster decision of first-order graph properties

Trade-off analysis meets probabilistic model checking

Content Provider	ACM Digital Library
Author	Dubslaff, Clemens Klüppelholz, Sascha Baier, Christel
Abstract	Probabilistic model checking (PMC) is a well-established and powerful method for the automated quantitative analysis of parallel distributed systems. Classical PMC-approaches focus on computing probabilities and expectations in Markovian models annotated with numerical values for costs and utility, such as energy and performance. Usually, the utility gained and the costs invested are dependent and a trade-off analysis is of utter interest. In this paper, we provide an overview on various kinds of non-standard multi-objective formalisms that enable to specify and reason about the trade-off between costs and utility. In particular, we present the concepts of quantiles, conditional probabilities and expectations as well as objectives on the ratio between accumulated costs and utility. Such multi-objective properties have drawn very few attention in the context of PMC and hence, there is hardly any tool support in state-of-the-art model checkers. Furthermore, we broaden our results towards combined quantile queries, computing conditional probabilities those conditions are expressed as formulas in probabilistic computation tree logic, and the computation of ratios which can be expected on the long-run.
Starting Page	1
Ending Page	10
Page Count	10
File Format	PDF
ISBN	9781450328869
DOI	10.1145/2603088.2603089
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-07-14
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in