Showing 1–19 of 19 results for author: Merz, S

On the Value of PHH3 for Mitotic Figure Detection on H&E-stained Images

Authors: Jonathan Ganz, Christian Marzahl, Jonas Ammeling, Barbara Richter, Chloé Puget, Daniela Denk, Elena A. Demeter, Flaviu A. Tabaran, Gabriel Wasinger, Karoline Lipnik, Marco Tecilla, Matthew J. Valentine, Michael J. Dark, Niklas Abele, Pompei Bolfa, Ramona Erber, Robert Klopfleisch, Sophie Merz, Taryn A. Donovan, Samir Jabari, Christof A. Bertram, Katharina Breininger, Marc Aubreville

Abstract: The count of mitotic figures (MFs) observed in hematoxylin and eosin (H&E)-stained slides is an important prognostic marker as it is a measure for tumor cell proliferation. However, the identification of MFs has a known low inter-rater agreement. Deep learning algorithms can standardize this task, but they require large amounts of annotated data for training and validation. Furthermore, label nois… ▽ More The count of mitotic figures (MFs) observed in hematoxylin and eosin (H&E)-stained slides is an important prognostic marker as it is a measure for tumor cell proliferation. However, the identification of MFs has a known low inter-rater agreement. Deep learning algorithms can standardize this task, but they require large amounts of annotated data for training and validation. Furthermore, label noise introduced during the annotation process may impede the algorithm's performance. Unlike H&E, the mitosis-specific antibody phospho-histone H3 (PHH3) specifically highlights MFs. Counting MFs on slides stained against PHH3 leads to higher agreement among raters and has therefore recently been used as a ground truth for the annotation of MFs in H&E. However, as PHH3 facilitates the recognition of cells indistinguishable from H&E stain alone, the use of this ground truth could potentially introduce noise into the H&E-related dataset, impacting model performance. This study analyzes the impact of PHH3-assisted MF annotation on inter-rater reliability and object level agreement through an extensive multi-rater experiment. We found that the annotators' object-level agreement increased when using PHH3-assisted labeling. Subsequently, MF detectors were evaluated on the resulting datasets to investigate the influence of PHH3-assisted labeling on the models' performance. Additionally, a novel dual-stain MF detector was developed to investigate the interpretation-shift of PHH3-assisted labels used in H&E, which clearly outperformed single-stain detectors. However, the PHH3-assisted labels did not have a positive effect on solely H&E-based models. The high performance of our dual-input detector reveals an information mismatch between the H&E and PHH3-stained images as the cause of this effect. △ Less

Submitted 28 June, 2024; originally announced June 2024.

Comments: 10 pages, 5 figures, 1 Table

Validating Traces of Distributed Programs Against TLA+ Specifications

Authors: Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz

Abstract: TLA+ is a formal language for specifying systems, including distributed algorithms, that is supported by powerful verification tools. In this work we present a framework for relating traces of distributed programs to high-level specifications written inTLA+. The problem is reduced to a constrained model checking problem, realized using the TLC model checker. Our framework consists of an API for in… ▽ More TLA+ is a formal language for specifying systems, including distributed algorithms, that is supported by powerful verification tools. In this work we present a framework for relating traces of distributed programs to high-level specifications written inTLA+. The problem is reduced to a constrained model checking problem, realized using the TLC model checker. Our framework consists of an API for instrumenting Java programs in order to record traces of executions, of a collection of TLA+ operators that are used for relating those traces to specifications, and of scripts for running the model checker.Crucially, traces only contain updates to specification variables rather than full values, and it is not necessary to provide values for all variables. We have applied our approach to several distributed programs, detecting discrepancies between the specifications and the implementations in all cases. We discuss reasons for these discrepancies, how to interpret the verdict produced by TLC, and how to take into account the results of trace validation for implementation development. △ Less

Submitted 23 April, 2024; originally announced April 2024.

Nuclear Pleomorphism in Canine Cutaneous Mast Cell Tumors: Comparison of Reproducibility and Prognostic Relevance between Estimates, Manual Morphometry and Algorithmic Morphometry

Authors: Andreas Haghofer, Eda Parlak, Alexander Bartel, Taryn A. Donovan, Charles-Antoine Assenmacher, Pompei Bolfa, Michael J. Dark, Andrea Fuchs-Baumgartinger, Andrea Klang, Kathrin Jäger, Robert Klopfleisch, Sophie Merz, Barbara Richter, F. Yvonne Schulman, Hannah Janout, Jonathan Ganz, Josef Scharinger, Marc Aubreville, Stephan M. Winkler, Matti Kiupel, Christof A. Bertram

Abstract: Variation in nuclear size and shape is an important criterion of malignancy for many tumor types; however, categorical estimates by pathologists have poor reproducibility. Measurements of nuclear characteristics (morphometry) can improve reproducibility, but manual methods are time consuming. The aim of this study was to explore the limitations of estimates and develop alternative morphometric sol… ▽ More Variation in nuclear size and shape is an important criterion of malignancy for many tumor types; however, categorical estimates by pathologists have poor reproducibility. Measurements of nuclear characteristics (morphometry) can improve reproducibility, but manual methods are time consuming. The aim of this study was to explore the limitations of estimates and develop alternative morphometric solutions for canine cutaneous mast cell tumors (ccMCT). We assessed the following nuclear evaluation methods for measurement accuracy, reproducibility, and prognostic utility: 1) anisokaryosis (karyomegaly) estimates by 11 pathologists; 2) gold standard manual morphometry of at least 100 nuclei; 3) practicable manual morphometry with stratified sampling of 12 nuclei by 9 pathologists; and 4) automated morphometry using a deep learning-based segmentation algorithm. The study dataset comprised 96 ccMCT with available outcome information. The study dataset comprised 96 ccMCT with available outcome information. Inter-rater reproducibility of karyomegaly estimates was low ($κ$ = 0.226), while it was good (ICC = 0.654) for practicable morphometry of the standard deviation (SD) of nuclear size. As compared to gold standard manual morphometry (AUC = 0.839, 95% CI: 0.701 - 0.977), the prognostic value (tumor-specific survival) of SDs of nuclear area for practicable manual morphometry (12 nuclei) and automated morphometry were high with an area under the ROC curve (AUC) of 0.868 (95% CI: 0.737 - 0.991) and 0.943 (95% CI: 0.889 - 0.996), respectively. This study supports the use of manual morphometry with stratified sampling of 12 nuclei and algorithmic morphometry to overcome the poor reproducibility of estimates. △ Less

Submitted 23 May, 2024; v1 submitted 26 September, 2023; originally announced September 2023.

Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS

Authors: Igor Konnov, Markus Kuppe, Stephan Merz

Abstract: Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their complementary strengths and weaknesses, we suggest a workflow that supports different types of analysis and that can be adapted to the desired degree of confidence. Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their complementary strengths and weaknesses, we suggest a workflow that supports different types of analysis and that can be adapted to the desired degree of confidence. △ Less

Submitted 14 November, 2022; originally announced November 2022.

Journal ref: Leveraging Applications of Formal Methods, Verification and Validation. 11th International Symposium, ISoLA 2022, 2022, Rhodes, Greece. pp.88-105

Failing to hash into supersingular isogeny graphs

Authors: Jeremy Booher, Ross Bowden, Javad Doliskani, Tako Boris Fouotsa, Steven D. Galbraith, Sabrina Kunzweiler, Simon-Philipp Merz, Christophe Petit, Benjamin Smith, Katherine E. Stange, Yan Bo Ti, Christelle Vincent, José Felipe Voloch, Charlotte Weitkämper, Lukas Zobernig

Abstract: An important open problem in supersingular isogeny-based cryptography is to produce, without a trusted authority, concrete examples of "hard supersingular curves" that is, equations for supersingular curves for which computing the endomorphism ring is as difficult as it is for random supersingular curves. A related open problem is to produce a hash function to the vertices of the supersingular… ▽ More An important open problem in supersingular isogeny-based cryptography is to produce, without a trusted authority, concrete examples of "hard supersingular curves" that is, equations for supersingular curves for which computing the endomorphism ring is as difficult as it is for random supersingular curves. A related open problem is to produce a hash function to the vertices of the supersingular $\ell$-isogeny graph which does not reveal the endomorphism ring, or a path to a curve of known endomorphism ring. Such a hash function would open up interesting cryptographic applications. In this paper, we document a number of (thus far) failed attempts to solve this problem, in the hope that we may spur further research, and shed light on the challenges and obstacles to this endeavour. The mathematical approaches contained in this article include: (i) iterative root-finding for the supersingular polynomial; (ii) gcd's of specialized modular polynomials; (iii) using division polynomials to create small systems of equations; (iv) taking random walks in the isogeny graph of abelian surfaces; and (v) using quantum random walks. △ Less

Submitted 8 May, 2024; v1 submitted 29 April, 2022; originally announced May 2022.

Comments: 34 pages, 8 figures

MSC Class: 11G05; 11T71; 14G50; 14K02; 81P94; 94A60; 68Q12

How Many Annotators Do We Need? -- A Study on the Influence of Inter-Observer Variability on the Reliability of Automatic Mitotic Figure Assessment

Authors: Frauke Wilm, Christof A. Bertram, Christian Marzahl, Alexander Bartel, Taryn A. Donovan, Charles-Antoine Assenmacher, Kathrin Becker, Mark Bennett, Sarah Corner, Brieuc Cossic, Daniela Denk, Martina Dettwiler, Beatriz Garcia Gonzalez, Corinne Gurtner, Annika Lehmbecker, Sophie Merz, Stephanie Plog, Anja Schmidt, Rebecca C. Smedley, Marco Tecilla, Tuddow Thaiwong, Katharina Breininger, Matti Kiupel, Andreas Maier, Robert Klopfleisch , et al. (1 additional authors not shown)

Abstract: Density of mitotic figures in histologic sections is a prognostically relevant characteristic for many tumours. Due to high inter-pathologist variability, deep learning-based algorithms are a promising solution to improve tumour prognostication. Pathologists are the gold standard for database development, however, labelling errors may hamper development of accurate algorithms. In the present work… ▽ More Density of mitotic figures in histologic sections is a prognostically relevant characteristic for many tumours. Due to high inter-pathologist variability, deep learning-based algorithms are a promising solution to improve tumour prognostication. Pathologists are the gold standard for database development, however, labelling errors may hamper development of accurate algorithms. In the present work we evaluated the benefit of multi-expert consensus (n = 3, 5, 7, 9, 11) on algorithmic performance. While training with individual databases resulted in highly variable F$_1$ scores, performance was notably increased and more consistent when using the consensus of three annotators. Adding more annotators only resulted in minor improvements. We conclude that databases by few pathologists and high label accuracy may be the best compromise between high algorithmic performance and time investment. △ Less

Submitted 8 January, 2021; v1 submitted 4 December, 2020; originally announced December 2020.

Comments: Due to data inconsistencies experiments had to be repeated with a reduced number of annotators (17 in version 1). All findings of the previous version were reproducible. 7 pages, 2 figures, accepted at BVM workshop 2021

Are fast labeling methods reliable? A case study of computer-aided expert annotations on microscopy slides

Authors: Christian Marzahl, Christof A. Bertram, Marc Aubreville, Anne Petrick, Kristina Weiler, Agnes C. Gläsel, Marco Fragoso, Sophie Merz, Florian Bartenschlager, Judith Hoppe, Alina Langenhagen, Anne Jasensky, Jörn Voigt, Robert Klopfleisch, Andreas Maier

Abstract: Deep-learning-based pipelines have shown the potential to revolutionalize microscopy image diagnostics by providing visual augmentations to a trained pathology expert. However, to match human performance, the methods rely on the availability of vast amounts of high-quality labeled data, which poses a significant challenge. To circumvent this, augmented labeling methods, also known as expert-algori… ▽ More Deep-learning-based pipelines have shown the potential to revolutionalize microscopy image diagnostics by providing visual augmentations to a trained pathology expert. However, to match human performance, the methods rely on the availability of vast amounts of high-quality labeled data, which poses a significant challenge. To circumvent this, augmented labeling methods, also known as expert-algorithm-collaboration, have recently become popular. However, potential biases introduced by this operation mode and their effects for training neuronal networks are not entirely understood. This work aims to shed light on some of the effects by providing a case study for three pathologically relevant diagnostic settings. Ten trained pathology experts performed a labeling tasks first without and later with computer-generated augmentation. To investigate different biasing effects, we intentionally introduced errors to the augmentation. Furthermore, we developed a novel loss function which incorporates the experts' annotation consensus in the training of a deep learning classifier. In total, the pathology experts annotated 26,015 cells on 1,200 images in this novel annotation study. Backed by this extensive data set, we found that the consensus of multiple experts and the deep learning classifier accuracy, was significantly increased in the computer-aided setting, versus the unaided annotation. However, a significant percentage of the deliberately introduced false labels was not identified by the experts. Additionally, we showed that our loss function profited from multiple experts and outperformed conventional loss functions. At the same time, systematic errors did not lead to a deterioration of the trained classifier accuracy. Furthermore, a classifier trained with annotations from a single expert with computer-aided support can outperform the combined annotations from up to nine experts. △ Less

Submitted 13 April, 2020; originally announced April 2020.

Comments: 10 pages, send to MICCAI 2020

Deep learning algorithms out-perform veterinary pathologists in detecting the mitotically most active tumor region

Authors: Marc Aubreville, Christof A. Bertram, Christian Marzahl, Corinne Gurtner, Martina Dettwiler, Anja Schmidt, Florian Bartenschlager, Sophie Merz, Marco Fragoso, Olivia Kershaw, Robert Klopfleisch, Andreas Maier

Abstract: Manual count of mitotic figures, which is determined in the tumor region with the highest mitotic activity, is a key parameter of most tumor grading schemes. It can be, however, strongly dependent on the area selection due to uneven mitotic figure distribution in the tumor section.We aimed to assess the question, how significantly the area selection could impact the mitotic count, which has a know… ▽ More Manual count of mitotic figures, which is determined in the tumor region with the highest mitotic activity, is a key parameter of most tumor grading schemes. It can be, however, strongly dependent on the area selection due to uneven mitotic figure distribution in the tumor section.We aimed to assess the question, how significantly the area selection could impact the mitotic count, which has a known high inter-rater disagreement. On a data set of 32 whole slide images of H&E-stained canine cutaneous mast cell tumor, fully annotated for mitotic figures, we asked eight veterinary pathologists (five board-certified, three in training) to select a field of interest for the mitotic count. To assess the potential difference on the mitotic count, we compared the mitotic count of the selected regions to the overall distribution on the slide.Additionally, we evaluated three deep learning-based methods for the assessment of highest mitotic density: In one approach, the model would directly try to predict the mitotic count for the presented image patches as a regression task. The second method aims at deriving a segmentation mask for mitotic figures, which is then used to obtain a mitotic density. Finally, we evaluated a two-stage object-detection pipeline based on state-of-the-art architectures to identify individual mitotic figures. We found that the predictions by all models were, on average, better than those of the experts. The two-stage object detector performed best and outperformed most of the human pathologists on the majority of tumor cases. The correlation between the predicted and the ground truth mitotic count was also best for this approach (0.963 to 0.979). Further, we found considerable differences in position selection between pathologists, which could partially explain the high variance that has been reported for the manual mitotic count. △ Less

Submitted 21 October, 2020; v1 submitted 12 February, 2019; originally announced February 2019.

Comments: 13 pages, 7 figures

Journal ref: Sci Rep. 2020 Oct 5;10(1):16447

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle

Authors: Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery

Abstract: Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle. Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle. △ Less

Submitted 29 October, 2018; originally announced October 2018.

Auxiliary Variables in TLA+

Authors: Leslie Lamport, Stephan Merz

Abstract: Auxiliary variables are often needed for verifying that an implementation is correct with respect to a higher-level specification. They augment the formal description of the implementation without changing its semantics--that is, the set of behaviors that it describes. This paper explains rules for adding history, prophecy, and stuttering variables to TLA+ specifications, ensuring that the augment… ▽ More Auxiliary variables are often needed for verifying that an implementation is correct with respect to a higher-level specification. They augment the formal description of the implementation without changing its semantics--that is, the set of behaviors that it describes. This paper explains rules for adding history, prophecy, and stuttering variables to TLA+ specifications, ensuring that the augmented specification is equivalent to the original one. The rules are explained with toy examples, and they are used to verify the correctness of a simplified version of a snapshot algorithm due to Afek et al. △ Less

Submitted 29 May, 2017; v1 submitted 15 March, 2017; originally announced March 2017.

Encoding TLA+ set theory into many-sorted first-order logic

Authors: Stephan Merz, Hernán Vanzetto

Abstract: We present an encoding of Zermelo-Fraenkel set theory into many-sorted first-order logic, the input language of state-of-the-art SMT solvers. This translation is the main component of a back-end prover based on SMT solvers in the TLA+ Proof System. We present an encoding of Zermelo-Fraenkel set theory into many-sorted first-order logic, the input language of state-of-the-art SMT solvers. This translation is the main component of a back-end prover based on SMT solvers in the TLA+ Proof System. △ Less

Submitted 16 August, 2015; originally announced August 2015.

Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations

Authors: **gshu Chen, Marie Duflot, Stephan Merz

Abstract: Avoiding access conflicts is a major challenge in the design of multi-threaded programs. In the context of real-time systems, the absence of conflicts can be guaranteed by ensuring that no two potentially conflicting accesses are ever scheduled concurrently.In this paper, we analyze programs that carry time annotations specifying the time for executing each statement. We propose a technique for ve… ▽ More Avoiding access conflicts is a major challenge in the design of multi-threaded programs. In the context of real-time systems, the absence of conflicts can be guaranteed by ensuring that no two potentially conflicting accesses are ever scheduled concurrently.In this paper, we analyze programs that carry time annotations specifying the time for executing each statement. We propose a technique for verifying that a multi-threaded program with time annotations is free of access conflicts. In particular, we generate constraints that reflect the possible schedules for executing the program and the required properties. We then invoke an SMT solver in order to verify that no execution gives rise to concurrent conflicting accesses. Otherwise, we obtain a trace that exhibits the access conflict. △ Less

Submitted 30 November, 2014; originally announced December 2014.

Comments: http://journal.ub.tu-berlin.de/eceasst/article/view/978

Journal ref: Electronic Communications of the EASST, 2014, Automated Verification of Critical Systems 2014, 70, pp.14

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

Authors: Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz

Abstract: We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic. We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic. △ Less

Submitted 12 September, 2014; originally announced September 2014.

Comments: appears in Automated Reasoning in Quantified Non-Classical Logics (2014)

TLA+ Proofs

Authors: Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, Hernán Vanzetto

Abstract: TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual exclusion algorithm as a simple example to describe the features of TLAPS and show how it and the Toolbox (an IDE for TLA+) help users to manage large, complex pr… ▽ More TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual exclusion algorithm as a simple example to describe the features of TLAPS and show how it and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs. △ Less

Submitted 29 August, 2012; originally announced August 2012.

Comments: A shorter version of this article appeared in the proceedings of the conference Formal Methods 2012 (FM 2012, Paris, France, Springer LNCS 7436, pp. 147-154)

ACM Class: D.2.4; F.3.1

Verifying Safety Properties With the TLA+ Proof System

Authors: Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz

Abstract: TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem p… ▽ More TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. This paper documents the first public release of TLAPS, distributed with a BSD-like license. It handles almost all the non-temporal part of TLA+ as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties. △ Less

Submitted 11 November, 2010; originally announced November 2010.

Journal ref: Fifth International Joint Conference on Automated Reasoning (IJCAR), Edinburgh : United Kingdom (2010)

A Formalization of the Semantics of Functional-Logic Programming in Isabelle

Authors: Francisco López Fraguas, Stephan Merz, Juan Rodríguez Hortalá

Abstract: Modern functional-logic programming languages like Toy or Curry feature non-strict non-deterministic functions that behave under call-time choice semantics. A standard formulation for this semantics is the CRWL logic, that specifies a proof calculus for computing the set of possible results for each expression. In this paper we present a formalization of that calculus in the Isabelle/HOL proof a… ▽ More Modern functional-logic programming languages like Toy or Curry feature non-strict non-deterministic functions that behave under call-time choice semantics. A standard formulation for this semantics is the CRWL logic, that specifies a proof calculus for computing the set of possible results for each expression. In this paper we present a formalization of that calculus in the Isabelle/HOL proof assistant. We have proved some basic properties of CRWL: closedness under c-substitutions, polarity and compositionality. We also discuss some insights that have been gained, such as the fact that left linearity of program rules is not needed for any of these results to hold. △ Less

Submitted 4 August, 2009; originally announced August 2009.

Journal ref: 22nd International Conference Theorem Proving for Higher-Order Logics (TPHOLs 2009): emerging trends session (2009)

A TLA+ Proof System

Authors: Kaustuv C. Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz

Abstract: We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The language and the PM support the incremental development and checking of hierarchically structured proofs. The PM translates a proof into a set of independent proof obligations and calls upon a collection of back-end pro… ▽ More We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The language and the PM support the incremental development and checking of hierarchically structured proofs. The PM translates a proof into a set of independent proof obligations and calls upon a collection of back-end provers to verify them. Different provers can be used to verify different obligations. The currently supported back-ends are the tableau prover Zenon and Isabelle/TLA+, an axiomatisation of TLA+ in Isabelle/Pure. The proof obligations for a complete TLA+ proof can also be used to certify the theorem in Isabelle/TLA+. △ Less

Submitted 12 November, 2008; originally announced November 2008.

Journal ref: Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA) (2008)

Event Systems and Access Control

Authors: Dominique Méry, Stephan Merz

Abstract: We consider the interpretations of notions of access control (permissions, interdictions, obligations, and user rights) as run-time properties of information systems specified as event systems with fairness. We give proof rules for verifying that an access control policy is enforced in a system, and consider preservation of access control by refinement of event systems. In particular, refinement… ▽ More We consider the interpretations of notions of access control (permissions, interdictions, obligations, and user rights) as run-time properties of information systems specified as event systems with fairness. We give proof rules for verifying that an access control policy is enforced in a system, and consider preservation of access control by refinement of event systems. In particular, refinement of user rights is non-trivial; we propose to combine low-level user rights and system obligations to implement high-level user rights. △ Less

Submitted 21 April, 2006; originally announced April 2006.

Truly On-The-Fly LTL Model Checking

Authors: Moritz Hammer, Alexander Knapp, Stephan Merz

Abstract: We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized Büchi automaton for the negation of the formula and the emptiness check. Our algorithm first converts the LTL formula into a linear weak alternating automaton; configurations of the alternating automaton correspond to the locations of a generalized Büchi automaton, and a varian… ▽ More We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized Büchi automaton for the negation of the formula and the emptiness check. Our algorithm first converts the LTL formula into a linear weak alternating automaton; configurations of the alternating automaton correspond to the locations of a generalized Büchi automaton, and a variant of Tarjan's algorithm is used to decide the existence of an accepting run of the product of the transition system and the automaton. Because we avoid an explicit construction of the Büchi automaton, our approach can yield significant improvements in runtime and memory, for large LTL formulas. The algorithm has been implemented within the SPIN model checker, and we present experimental results for some benchmark examples. △ Less

Submitted 16 November, 2005; originally announced November 2005.

Journal ref: Dans Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005)