Publications
143 results found
Huth M, Piterman N, Wagner D, 2009, Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL, 17th International Symposium on Fundamentals of Computation Theory, Publisher: SPRINGER-VERLAG BERLIN, Pages: 205-216, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 4
Huth M, Piterman N, Wang H, 2009, A workbench for preprocessor design and evaluation: toward benchmarks for parity games\r\n, Ninth International Workshop on Automatic Verification of Critical Systems, Publisher: European Association of Software Science and Technology
We describe a prototype workbench for the study of parity games and their solvers. This workbench is aimed at facilitating two activities: to aid in the design, validation, and evaluation of pre-processors for parity game solvers; and to aid in the generation of benchmark parity games that are meaningful for a wide range of solvers. Our workbench allows for easy composition of pre-processors, can populate databases with games and their meta-data, offers a query language for generating games of interest, and has already found potentially hard games.\r\n
Wagner D, Piterman N, Huth M, et al., 2009, PCTL Model Checking of Markov Chains: Truth and Falsity as Winning Strategies in Games, Performance Evaluation, Vol: 67, Pages: 858-872, ISSN: 0166-5316
Probabilistic model checking is a technique for verifying whether a model such as a Markov chain satisfies a probabilistic, behavioral property û e.g. ôwith probability at least 0.999, a device will be elected leader.ö Such properties are expressible in probabilistic temporal logics, e.g. PCTL, and efficient algorithms exist for checking whether these formulae are true or false on infinite-state models. Alas, these algorithms do not supply diagnostic information for why a probabilistic property does or does not hold in a given model. We provide here complete and rigorous foundations for such diagnostics in the setting of countable labeled Markov chains and PCTL. For each model and PCTL formula, we define a game between a Verifier and a Refuter that is won by Verifier if the formula holds in the model, and won by Refuter if it does not hold. Games are won by exactly one player, through monotone strategies that encode the diagnostic information for truth and falsity (respectively). These games are infinite with Buechi type acceptance conditions where simpler fairness conditions are shown to be not sufficient. Verifier can always force finite plays for certain PCTL formulae, suggesting the existence of finite-state abstractions of models that satisfy such formulae. \r\n
Antonik A, Huth M, Larsen K, et al., 2008, EXPTIME-complete Decision Problems for Mixed and Modal Specifications, Electronic Notes in Theoretical Computer Science, Vol: 242, Pages: 19-33, ISSN: 1571-0661
Mixed and modal transition systems are formalisms allowing mixing of over- and under-approximation in a single specification. We show EXPTIME-completeness of three fundamental decision problems for such specifications: whether a set of mixed or modal specifications has a common implementation, whether a sole mixed specification has an implementation, and whether all implementations of one mixed specification are implementations of another mixed or modal one. These results are obtained by a chain of reductions starting with the acceptance problem for linearly bounded alternating Turing machines.\r\n
Bruns G, Huth M, 2008, Access-Control Policies via Belnap Logic: Effective and Efficient Composition and Analysis, 21st IEEE Computer Security Foundations Symposium, Publisher: IEEE Computer Society Press, Pages: 163-176
It is difficult to develop and manage large, multi-author access control policies without a means to compose larger policies from smaller ones. Ideally, an access-control policy language will have a small set of simple policy combinators that allow for all desired policy compositions. In [5], a policy language was presented having policy combinators based on Belnap logic, a four-valued logic in which truth values correspond to policy results of ôgrantö, ôdenyö, ôconflictö, and ôundefinedö. We show here how policies in this language can be analyzed, and study the expressiveness of the language. To support policy analysis, we define a query language in which policy analysis questions can be phrased. Queries can be translated into a fragment of first-order logic for which satisfiability and validity checks are computable by SAT solvers or BDDs. We show how policy analysis can then be carried out through model checking, validity checking, and assume-guarantee reasoning over such translated queries. We also present static analysis methods for the particular questions of whether policies contain gaps or conflicts. Finally, we establish expressiveness results showing that all data independent policies can be expressed in our policy language.\r\n
Antonik A, Huth M, Larsen K, et al., 2008, 20 Years of Mixed and Modal Specifications, EATCS Bulletin, Vol: 95, Pages: 94-129, ISSN: 0252-9742
Twenty years ago, modal and mixed specifications were proposed as abstract models of system behavior. In this paper, we explain the nature and utility of such specifications, relate them to other formalisms, showcase some of their established applications, and mention some existing tool support. We also present some recent complexity results for decision problems underlying such applications and list some remaining open problems.\r\n \r\n
Huth M, Antonik A, Nyman U, et al., 2008, Complexity of decision problems for mixed and modal transition systems, FOSSACS 2008, Publisher: Springer Verlag
We consider decision problems for modal and mixed transition systems used as specifications: the common implementation problem (whether a set of specifications has a common implementation), the consistency problem (whether a single specification has an implementation), and the thorough refinement problem (whether all implementations of one specification are also implementations of another one). Common implementation and thorough refinement are shown to be PSPACE hard for modal, and so also for mixed, specifications. Consistency is PSPACE hard for mixed, while trivial for modal specifications. We also supply upper bounds suggesting strong links between these problems.\r\n\r\n
Hussain A, Huth M, 2008, On model checking multiple hybrid views, Theoretical Computer Science
Fecher H, Huth M, Piterman N, et al., 2008, Hintikka Games for PCTL on Labeled Markov Chains, 5th International Conference on the Quantitative Evaluation of Systems, Publisher: IEEE COMPUTER SOC, Pages: 169-+
- Author Web Link
- Cite
- Citations: 2
Fecher H, Huth M, 2008, Model checking for action abstraction, 9th International Conference on Verification, Model Checking, and Abstract Interpretation, Publisher: SPRINGER-VERLAG BERLIN, Pages: 112-126, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 2
Antonik A, Huth M, Larsen KG, et al., 2008, Complexity of decision problems for mixed and modal specifications, 11th International Conference on Foundations of Software Science and Computational Structures, Publisher: SPRINGER-VERLAG BERLIN, Pages: 112-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 18
Antonik A, Huth M, 2008, On the complexity of semantic self-minimization, Electronic Notes in Theoretical Computer Science, Vol: 250, Pages: 3-19, ISSN: 1571-0661
Partial Kripke structures model only parts of a state space and so enable aggressive abstraction of systems prior to verifying them with respect to a formula of temporal logic. This partiality of models means that verifications may reply with true (all refinements satisfy the formula under check), false (no refinement satisfies the formula under check) or donÆt know. Generalized model checking is the most precise verification for such models (all donÆt know answers imply that some refinements satisfy the formula, some donÆt), but computationally expensive. A compositional model-checking algorithm for partial Kripke structures is efficient, sound (all answers true and false are truthful), but may lose precision by answering donÆt know instead of a factual true or false. Recent work has shown that such a loss of precision does not occur for this compositional algorithm for most practically relevant patterns of temporal logic formulas. Formulas that never lose precision in this manner are called semantically self-minimizing. In this paper we provide a systematic study of the complexity of deciding whether a formula of propositional logic, propositional modal logic or the propositional modal mu-calculus is semantically self-minimizing.\r\n
Fecher H, Huth M, Schmidt H, et al., 2008, Refinement sensitive formal semantics of state machines with persistent choice, Electronic Notes in Theoretical Computer Science, Vol: 250, Pages: 71-86, ISSN: 1571-0661
Modeling languages usually support two kinds of nondeterminism, an external one for interactions of a system with its environment, and one that stems from under-specification as familiar in models of behavioral requirements. Both forms of nondeterminism are resolvable by composing a system with an environment model and by refining under-specified behavior (respectively). Modeling languages usually donÆt support nondeterminism that is persistent in that neither the composition with an environment nor refinements of under-specification will resolve it. Persistent nondeterminism is used, e.g., for modeling faulty systems. We present a formal semantics for UML state machines enriched with an operator ôpersistent choiceö that models persistent nondeterminism. This semantics is based on abstract models (mu-automata with a novel refinement relation) and a sound three-valued satisfaction relation for properties expressed in the mu-calculus.\r\n
Ryan M, Huth M, 2008, Logic in Computer Science: modelling and reasoning about systems (Portuguese language edition)\r\n, Publisher: Cambridge University Press, ISBN: 9-788-521-616108
Huth M, Charlton N, 2008, Falsifying safety properties through games on over-approximating models\r\n, Electronic Notes in Theoretical Computer Science, Vol: 223, Pages: 71-86, ISSN: 1571-0661
Abstractions of programs are traditionally over-approximations and have proved to be useful for the verification of safety properties. They are presently perceived as being useless for the falsification of safety properties, i.e. showing that program execution definitely reaches a ôbadö state. Alternative techniques, such as the computation of under-approximating must transitions, have addressed this shortcoming in the past. We show that over-approximating models can indeed falsify safety properties by relying on and exploiting the seriality and partial determinism of programs: programs donÆt just stop for no reason, and most program statements have deterministic semantics. Our method is based on solving a two-person attractor game derived from over-approximating models and makes no assumptions about the abstraction domain used. An example demonstrates the successful use of our approach, and highlights the role played by seriality and our handling of nondeterminism. Finally, we show that our method can encode must transitions, if supplied, by a simple modification of the ownership of nodes in the attractor game derived from the over-approximating model.\r\n
Dantas D, Bruns G, Huth M, 2007, A simple and expressive semantic framework for policy composition in access control\r\n, FMSE 2007, Publisher: ACM Press, Pages: 12-21
In defining large, complex access control policies, one would like to compose sub-policies, perhaps authored by different organizations, into a single global policy. Existing policy composition approaches tend to be ad-hoc, and do not explain whether too many or too few policy combinators have been defined. We define an access control policy as a *four-valued* predicate that maps accesses to either *grant*, *deny*, *conflict*, or *unspecified*. These correspond to the four elements of the Belnap bilattice. Functions on this bilattice are then extended to policies to serve as policy combinators. We argue that this approach provides a simple and natural semantic framework for policy composition, with a minimal but functionally complete set of policy combinators. We define derived, higher-level operators that are convenient for the specification of access control policies, and enable the decoupling of conflict resolution from policy composition. Finally, we propose a basic query language and show that it can reduce important analyses (e.g. conflict analysis) to checks of policy refinement.\r\n\r\n\r\n\r\n
Charlton N, Huth M, 2007, Hector: software model checking with cooperating analysis plugins, Computer Aided Verification (CAV 2007), Publisher: Springer
We present Hector, a software tool for combining different abstraction methods to extract sound models of heap-manipulating imperative programs with recursion. Extracted models may be explored visually and model checked with a wide range of ôpropositionalö temporal logic safety properties, where ôpropositionsö are formulae of a first order logic with transitive closure and arithmetic (L). Hector uses techniques initiated in [4, 5] to wrap up different abstraction methods as modular analysis plugins, and to exchange information about program state between plugins through formulae of L. This approach aims to achieve both (apparently conflicting) advantages of increased precision and modularity. When checking safety properties containing non-independent ôpropositionsö,\r\nour model checking algorithm gives greater precision than a naıve three-valued one since it maintains some dependencies.
Charlton N, Huth M, 2007, Cleanly combining specialised program analysers, Automated Reasoning Workshop 2007
Automatically proving that (infinite-state) software programs satisfy a specification is an important task, but has proved very difficult. Thus, in order to obtain techniques that work with reasonable speed and without user guidance, researchers have typically targeted restricted classes of language features, programming idioms and properties. We have designed a system in which several of these specialised techniques can be used together in proving that a program is correct; this is done without breaking modularity by propagating information between the analyses, expressed as formulae of an expressive common logic. In this way, we can verify programs which, because they use diverse language features and idioms, are difficult or impossible to prove using any one individual technique. Our system is implemented in the experimental tool HECTOR.
Fecher H, Huth M, 2007, More precise partition abstractions, Verification, Model Checking, and Abstract Interpretation, Publisher: Springer Verlag, Pages: 167-181, ISSN: 0302-9743
Huth M, 2007, Some current issues in model checking, Int J Softw Tools Technol Transfer, Vol: 9, Pages: 25-36, ISSN: 1433-2779
Fecher H, Huth M, 2006, Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise, Fourth international symposium on Automated Technology for Verification and Analysis, 23-26 October 2006, Beijing, China, Publisher: Springer Verlag, Pages: 322-336
Antonik A, Charlton NA, Huth M, 2006, Computing safe winning regions of parity games in polynomial time, Fourth Irish Conference on the Mathematical Foundations of Computer Science and Information Technology'06, MFCSIT'06, 1-5 August 2006, Cork, Ireland
Hussain A, Huth M, 2006, Automata games for multiple-model checking, Electronic Notes in Theoretical Computer Science, Vol: 155, Pages: 401-421
Antonik A, Huth M, 2006, Efficient Patterns for Model Checking Partial State Spaces in CTL & LTL, Electronic Notes in Theoretical Computer Science, Vol: 158, Pages: 41-57
Fecher H, Huth M, 2006, Complete abstractions through extensions of disjunctive modal transition systems, Complete abstractions through extensions of disjunctive modal transition systems
Antonik A, Carhlton N, Huth M, 2006, Polynomial-time under-approximation of winning regions in parity games, Departmental Technical Report: 06/12, Publisher: Department of Computing, Imperial College London, 06/12
We propose a pattern for designing algorithms that run in polynomial time by construction and underapproximatethe winning regions of both players in parity games. This approximation is achieved by theinteraction of finitely many aspects governed by a common ranking function, where the choice of aspects andranking function instantiates the design pattern. Each aspect attempts to improve the under-approximationof winning regions or decrease the rank function by simplifying the structure of the parity game. Our designpattern is incremental as aspects may operate on the residual game of yet undecided nodes. We presentseveral aspects and one higher-order transformation of our algorithms—based on efficient, static analyses—and illustrate the benefit of their interaction as well as their relative precision within pattern instantiations.Instantiations of our design pattern can be applied for local model checking and as pre-processors foralgorithms whose worst-case running time is exponential.
Huth M, 2006, Topological analysis of refinement, Electronic Notes in Theoretical Computer Science, Vol: 161, Pages: 3-23
Huth M, 2005, On finite-state approximants for probabilistic computation tree logic, Theoretical Computer Science, Vol: 346, Pages: 113-134, ISSN: 0304-3975
Huth M, 2005, Refinement is complete for implementations, Formal Aspects of Computing, Vol: 17, Pages: 113-137, ISSN: 0934-5043
Huth M, 2005, Labelled transition systems as a stone space, Logical Methods in Computer Science, Vol: 1, Pages: 1-28, ISSN: 1860-5974
A fully abstract and universal domain model for modal transition systems and refinement is shown to be a maximal-points space model for the bisimulation quotient of labelled transition systems over a finite set of events. In this domain model we prove that this quotient is a Stone space whose compact, zero-dimensional, and ultra-metrizable Hausdorff topology measures the degree of bisimilarity such that image-finite labelled transition systems are dense. Using this compactness we show that the set of labelled transition systems that refine a modal transition system, its ''set of implementations'', is compact and derive a compactness theorem for Hennessy-Milner logic on such implementation sets. These results extend to systems that also have partially specified state propositions, unify existing denotational, operational, and metric semantics on partial processes, render robust consistency measures for modal transition systems, and yield an abstract interpretation of compact sets of labelled transition systems as Scott-closed sets of modal transition systems.
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.