MOSEL: A flexible toolset for Monadic Second-order Logic

被引:0
|
作者
Kelb, P
Margaria, T
Mendler, M
Gsottberger, C
机构
关键词
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
MOSEL is a new tool-set for the analysis and verification in Monadic Second-order Logic. In this paper we concentrate on the system's design: MOSEL is a tool-set to include a flexible set of decision procedures for several theories of the logic complemented by a variety of support components for input format translations, visualization, and interfaces to other logics and tools. The main distinguishing features of MOSEL are its layered approach to the logic, based on a formal semantics for a minimal subset, its modular design, and its integration in a heterogeneous analysis and verification environment.
引用
收藏
页码:183 / 202
页数:20
相关论文
共 50 条
  • [1] Monadic Second-Order Logic with Arbitrary Monadic Predicates
    Fijalkow, Nathanael
    Paperman, Charles
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2014, PT I, 2014, 8634 : 279 - 290
  • [2] Monadic Second-Order Logic with Arbitrary Monadic Predicates
    Fijalkow, Nathanael
    Paperman, Charles
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2017, 18 (03)
  • [3] Quantitative Monadic Second-Order Logic
    Kreutzer, Stephan
    Riveros, Cristian
    2013 28TH ANNUAL IEEE/ACM SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2013, : 113 - 122
  • [4] Computability by monadic second-order logic
    Engelfriet, Joost
    INFORMATION PROCESSING LETTERS, 2021, 167
  • [5] Asymptotic Monadic Second-Order Logic
    Blumensath, Achim
    Carton, Olivier
    Colcombet, Thomas
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2014, PT I, 2014, 8634 : 87 - +
  • [6] Monadic Second-Order Logic on Finite Sequences
    D'Antoni, Loris
    Veanes, Margus
    ACM SIGPLAN NOTICES, 2017, 52 (01) : 232 - 245
  • [7] On the Parameterised Intractability of Monadic Second-Order Logic
    Kreutzer, Stephan
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2009, 5771 : 348 - 363
  • [8] Circle graphs and monadic second-order logic
    LaBRI, Université Bordeaux 1, CNRS, 351 Cours de la libération, 33405 Talence Cedex, France
    Journal of Applied Logic, 2008, 6 (03) : 416 - 442
  • [9] ON THE PARAMETERIZED INTRACTABILITY OF MONADIC SECOND-ORDER LOGIC
    Kreutzer, Stephan
    LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (01)
  • [10] On translations of temporal logic of actions into monadic second-order logic
    Rabinovich, A
    THEORETICAL COMPUTER SCIENCE, 1998, 193 (1-2) : 197 - 214