Skip to main content

Showing 1–23 of 23 results for author: Volk, M

Searching in archive cs. Search in all archives.
.
  1. arXiv:2403.17862   

    cs.LO cs.PL cs.SE

    Proceedings Sixth Workshop on Models for Formal Analysis of Real Systems

    Authors: Frédéric Lang, Matthias Volk

    Abstract: This volume contains the proceedings of MARS 2024, the sixth workshop on Models for Formal Analysis of Real Systems, held as part of ETAPS 2024, the European Joint Conferences on Theory and Practice of Software. The MARS workshops bring together researchers from different communities who are developing formal models of real systems in areas where complex models occur, such as networks, cyber-phy… ▽ More

    Submitted 26 March, 2024; originally announced March 2024.

    Journal ref: EPTCS 399, 2024

  2. arXiv:2401.06574  [pdf, other

    cs.LO

    CTMCs with Imprecisely Timed Observations

    Authors: Thom Badings, Matthias Volk, Sebastian Junges, Marielle Stoelinga, Nils Jansen

    Abstract: Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring, we must incorporate past observations. The timing of these observations matters but may be uncertain. Thus, we consider a setting in which we are given a sequence of imprecisely timed labels called the evidence. The problem is to compute r… ▽ More

    Submitted 29 January, 2024; v1 submitted 12 January, 2024; originally announced January 2024.

    Comments: Extended version (with appendix) of the paper accepted at TACAS 2024

  3. arXiv:2308.06306  [pdf, other

    cs.CV eess.IV

    Towards Packaging Unit Detection for Automated Palletizing Tasks

    Authors: Markus Völk, Kilian Kleeberger, Werner Kraus, Richard Bormann

    Abstract: For various automated palletizing tasks, the detection of packaging units is a crucial step preceding the actual handling of the packaging units by an industrial robot. We propose an approach to this challenging problem that is fully trained on synthetically generated data and can be robustly applied to arbitrary real world packaging units without further training or setup effort. The proposed app… ▽ More

    Submitted 11 August, 2023; originally announced August 2023.

  4. Sampling-Based Verification of CTMCs with Uncertain Rates

    Authors: Thom S. Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga, Matthias Volk

    Abstract: We employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while the parameters allow dependencies between transition rates. Sampling the parameter values from the prior distribution then yields a standard CTMC, for which we may compute relevant reachability probabilities. We provide a… ▽ More

    Submitted 21 June, 2022; v1 submitted 17 May, 2022; originally announced May 2022.

    Journal ref: Computed Aided Verification (CAV) 2022

  5. arXiv:2203.11008  [pdf, other

    cs.CV cs.CL

    Transformer-based HTR for Historical Documents

    Authors: Phillip Benjamin Ströbel, Simon Clematide, Martin Volk, Tobias Hodel

    Abstract: We apply the TrOCR framework to real-world, historical manuscripts and show that TrOCR per se is a strong model, ideal for transfer learning. TrOCR has been trained on English only, but it can adapt to other languages that use the Latin alphabet fairly easily and with little training material. We compare TrOCR against a SOTA HTR framework (Transkribus) and show that it can beat such systems. This… ▽ More

    Submitted 21 March, 2022; originally announced March 2022.

    Comments: This is an abstract submitted and accepted at ComHum 2022 in Lausanne. We will be elaborating on these initial findings in the paper that we will submit after the conference

  6. arXiv:2202.02829  [pdf, other

    cs.SE

    BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees

    Authors: Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan, Marielle Stoelinga

    Abstract: Fault trees are a key model in reliability analysis. Classical static fault trees (SFT) can best be analysed using binary decision diagrams (BDD). State-based techniques are favorable for the more expressive dynamic fault trees (DFT). This paper combines the best of both worlds by following Dugan's approach: dynamic sub-trees are analysed via model checking Markov models and replaced by basic even… ▽ More

    Submitted 28 March, 2022; v1 submitted 6 February, 2022; originally announced February 2022.

    Comments: Extended version of NFM'22 paper

  7. arXiv:2201.06170  [pdf, other

    cs.CL

    Evaluation of HTR models without Ground Truth Material

    Authors: Phillip Benjamin Ströbel, Simon Clematide, Martin Volk, Raphael Schwitter, Tobias Hodel, David Schoch

    Abstract: The evaluation of Handwritten Text Recognition (HTR) models during their development is straightforward: because HTR is a supervised problem, the usual data split into training, validation, and test data sets allows the evaluation of models in terms of accuracy or error rates. However, the evaluation process becomes tricky as soon as we switch from development to application. A compilation of a ne… ▽ More

    Submitted 29 April, 2022; v1 submitted 16 January, 2022; originally announced January 2022.

    Comments: Accepted at LREC 2022. Final version submitted to LREC 2022

  8. arXiv:2104.07528  [pdf, other

    cs.CV cs.AI cs.RO

    Investigations on Output Parameterizations of Neural Networks for Single Shot 6D Object Pose Estimation

    Authors: Kilian Kleeberger, Markus Völk, Richard Bormann, Marco F. Huber

    Abstract: Single shot approaches have demonstrated tremendous success on various computer vision tasks. Finding good parameterizations for 6D object pose estimation remains an open challenge. In this work, we propose different novel parameterizations for the output of the neural network for single shot 6D object pose estimation. Our learning-based approach achieves state-of-the-art performance on two public… ▽ More

    Submitted 15 April, 2021; originally announced April 2021.

    Comments: Accepted at 2021 IEEE International Conference on Robotics and Automation (ICRA 2021)

  9. arXiv:2101.04781  [pdf, other

    cs.RO cs.AI cs.CV

    Transferring Experience from Simulation to the Real World for Precise Pick-And-Place Tasks in Highly Cluttered Scenes

    Authors: Kilian Kleeberger, Markus Völk, Marius Moosmann, Erik Thiessenhusen, Florian Roth, Richard Bormann, Marco F. Huber

    Abstract: In this paper, we introduce a novel learning-based approach for grasping known rigid objects in highly cluttered scenes and precisely placing them based on depth images. Our Placement Quality Network (PQ-Net) estimates the object pose and the quality for each automatically generated grasp pose for multiple objects simultaneously at 92 fps in a single forward pass of a neural network. All grasping… ▽ More

    Submitted 12 January, 2021; originally announced January 2021.

    Comments: Accepted at 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2020)

  10. arXiv:2002.07080  [pdf, ps, other

    cs.SE

    The Probabilistic Model Checker Storm

    Authors: Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk

    Abstract: We present the probabilistic model checker Storm. Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the JANI and PRISM modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilist… ▽ More

    Submitted 6 October, 2020; v1 submitted 17 February, 2020; originally announced February 2020.

  11. arXiv:1906.01685  [pdf, ps, other

    cs.CL

    Post-editing Productivity with Neural Machine Translation: An Empirical Assessment of Speed and Quality in the Banking and Finance Domain

    Authors: Samuel Läubli, Chantal Amrhein, Patrick Düggelin, Beatriz Gonzalez, Alena Zwahlen, Martin Volk

    Abstract: Neural machine translation (NMT) has set new quality standards in automatic translation, yet its effect on post-editing productivity is still pending thorough investigation. We empirically test how the inclusion of NMT, in addition to domain-specific translation memories and termbases, impacts speed and quality in professional translation of financial texts. We find that even with language pairs t… ▽ More

    Submitted 4 June, 2019; originally announced June 2019.

    Comments: MT Summit 2019 (Research Track)

  12. arXiv:1903.07993  [pdf, other

    cs.LO eess.SY

    Parameter Synthesis for Markov Models: Covering the Parameter Space

    Authors: Sebastian Junges, Erika Ábrahám, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk

    Abstract: Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such as failure rates or packet loss ratios, etc. are often not -- or only partially -- known. This motivates considering parametric models with transitions labeled with functions over parameters. Whereas traditional Markov ch… ▽ More

    Submitted 7 November, 2023; v1 submitted 16 March, 2019; originally announced March 2019.

    Comments: 86 pages. Preprint of accepted FMSD Journal Paper

  13. Safety Analysis for Vehicle Guidance Systems with Dynamic Fault Trees

    Authors: Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk

    Abstract: This paper considers the design-phase safety analysis of vehicle guidance systems. The proposed approach constructs dynamic fault trees (DFTs) to model a variety of safety concepts and E/E architectures for drive automation. The fault trees can be used to evaluate various quantitative measures by means of model checking. The approach is accompanied by a large-scale evaluation: The resulting DFTs w… ▽ More

    Submitted 13 March, 2019; originally announced March 2019.

    Comments: Accepted in RESS

  14. arXiv:1808.07048  [pdf, ps, other

    cs.CL

    Has Machine Translation Achieved Human Parity? A Case for Document-level Evaluation

    Authors: Samuel Läubli, Rico Sennrich, Martin Volk

    Abstract: Recent research suggests that neural machine translation achieves parity with professional human translation on the WMT Chinese--English news translation task. We empirically test this claim with alternative evaluation protocols, contrasting the evaluation of single sentences and entire documents. In a pairwise ranking experiment, human raters assessing adequacy and fluency show a stronger prefere… ▽ More

    Submitted 21 August, 2018; originally announced August 2018.

    Comments: EMNLP 2018

  15. One Net Fits All: A unifying semantics of Dynamic Fault Trees using GSPNs

    Authors: Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk

    Abstract: Dynamic Fault Trees (DFTs) are a prominent model in reliability engineering. They are strictly more expressive than static fault trees, but this comes at a price: their interpretation is non-trivial and leaves quite some freedom. This paper presents a GSPN semantics for DFTs. This semantics is rather simple and compositional. The key feature is that this GSPN semantics unifies all existing DFT sem… ▽ More

    Submitted 14 March, 2018; originally announced March 2018.

    Comments: Accepted at Petri Nets 2018

  16. arXiv:1702.04311  [pdf, ps, other

    cs.SE

    A storm is Coming: A Modern Probabilistic Model Checker

    Authors: Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk

    Abstract: We launch the new probabilistic model checker storm. It features the analysis of discrete- and continuous-time variants of both Markov chains and MDPs. It supports the PRISM and JANI modeling languages, probabilistic programs, dynamic fault trees and generalized stochastic Petri nets. It has a modular set-up in which solvers and symbolic engines can easily be exchanged. It offers a Python API for… ▽ More

    Submitted 14 February, 2017; originally announced February 2017.

  17. arXiv:1610.08713  [pdf, ps, other

    cs.SE cs.LO cs.MS

    The Probabilistic Model Checker Storm (Extended Abstract)

    Authors: Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk

    Abstract: We present a new probabilistic model checker Storm. Using state-of-the-art libraries, we aim for both high performance and versatility. This extended abstract gives a brief overview of the features of Storm.

    Submitted 27 October, 2016; originally announced October 2016.

    Comments: Extended abstract

  18. Advancing Dynamic Fault Tree Analysis

    Authors: Matthias Volk, Sebastian Junges, Joost-Pieter Katoen

    Abstract: This paper presents a new state space generation approach for dynamic fault trees (DFTs) together with a technique to synthesise failures rates in DFTs. Our state space generation technique aggressively exploits the DFT structure --- detecting symmetries, spurious non-determinism, and don't cares. Benchmarks show a gain of more than two orders of magnitude in terms of state space generation and an… ▽ More

    Submitted 25 April, 2016; originally announced April 2016.

  19. arXiv:1405.6103  [pdf

    cs.CL

    Evaluating the fully automatic multi-language translation of the Swiss avalanche bulletin

    Authors: Kurt Winkler, Tobias Kuhn, Martin Volk

    Abstract: The Swiss avalanche bulletin is produced twice a day in four languages. Due to the lack of time available for manual translation, a fully automated translation system is employed, based on a catalogue of predefined phrases and predetermined rules of how these phrases can be combined to produce sentences. The system is able to automatically translate such sentences from German into the target langu… ▽ More

    Submitted 23 May, 2014; originally announced May 2014.

  20. arXiv:1312.3979  [pdf, ps, other

    cs.SE

    Accelerating Parametric Probabilistic Verification

    Authors: Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker

    Abstract: We present a novel method for computing reachability probabilities of parametric discrete-time Markov chains whose transition probabilities are fractions of polynomials over a set of parameters. Our algorithm is based on two key ingredients: a graph decomposition into strongly connected subgraphs combined with a novel factorization strategy for polynomials. Experimental evaluations show that these… ▽ More

    Submitted 27 March, 2014; v1 submitted 13 December, 2013; originally announced December 2013.

  21. arXiv:1206.0603  [pdf, other

    cs.SE

    The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains

    Authors: Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker

    Abstract: This report presents the tool COMICS, which performs model checking and generates counterexamples for DTMCs. For an input DTMC, COMICS computes an abstract system that carries the model checking information and uses this result to compute a critical subsystem, which induces a counterexample. This abstract subsystem can be refined and concretized hierarchically. The tool comes with a command-line v… ▽ More

    Submitted 4 June, 2012; originally announced June 2012.

  22. arXiv:cs/9811016  [pdf, ps, other

    cs.CL

    Comparing a statistical and a rule-based tagger for German

    Authors: Martin Volk, Gerold Schneider

    Abstract: In this paper we present the results of comparing a statistical tagger for German based on decision trees and a rule-based Brill-Tagger for German. We used the same training corpus (and therefore the same tag-set) to train both taggers. We then applied the taggers to the same test corpus and compared their respective behavior and in particular their error rates. Both taggers perform similarly wi… ▽ More

    Submitted 11 November, 1998; originally announced November 1998.

    Comments: 8 pages

    ACM Class: I.2.7

  23. Experiences with the GTU grammar development environment

    Authors: Martin Volk, Dirk Richarz

    Abstract: In this paper we describe our experiences with a tool for the development and testing of natural language grammars called GTU (German: Grammatik-Testumgebumg; grammar test environment). GTU supports four grammar formalisms under a window-oriented user interface. Additionally, it contains a set of German test sentences covering various syntactic phenomena as well as three types of German lexicons… ▽ More

    Submitted 21 July, 1997; originally announced July 1997.

    Comments: 7 pages, uses aclap.sty

    Journal ref: Proceedings of Workshop on Computational Environments For Grammar Development And Linguistic Engineering at the ACL/EACL Joint Conference 1997, 107-113