A Solving Procedure for Stochastic Satisfiability Modulo Theories with Continuous Domain

2015 ◽  
pp. 295-311 ◽  
Author(s):  
Yang Gao ◽  
Martin Fränzle
Keyword(s):  
Satisfiability Modulo Theories ◽  
Continuous Domain

scholarly journals Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain

10.29007/wm3j ◽  
2018 ◽  
Author(s):  
Yang Gao ◽  
Martin Fränzle
Keyword(s):  
Hybrid Systems ◽  
Markov Decision Processes ◽  
Stochastic Systems ◽  
Stochastic Game ◽  
Decision Processes ◽  
Satisfiability Modulo Theories ◽  
Hybrid State ◽  
Markov Decision ◽  
Discrete Domain ◽  
Continuous Domain

Stochastic Satisfiability Modulo Theories (SSMT) is a quantitative exten-sion of classical Satisfiability Modulo Theories (SMT) inspired by stochasticlogics. It extends SMT by the usual as well as randomized quantifiers, fa-cilitating capture of stochastic game properties in the logic, like reachabilityanalysis of hybrid-state Markov decision processes. Solving for SSMT for-mulae with quantification over finite and thus discrete domain has been ad-dressed by Tino Teige et al. In our work, we extend their work to SSMTover continuous quantifier domains (CSSMT) in order to enable capture of,e.g., continuous disturbances and uncertainty in hybrid systems. We extendthe semantics of SSMT and introduce a corresponding solving procedure. Adiscussion regarding to reachability analysis is given to demonstrate applica-bility of our framework to reachability problems in hybrid systems.

Engineering Theories with Z3

10.29007/x7b4 ◽  
2018 ◽  
Author(s):  
Nikolaj Bjorner
Keyword(s):  
Satisfiability Modulo Theories ◽  
Smt Solver ◽  
Testing Tools ◽  
Software And Hardware ◽  
Design And Testing

Modern Satisfiability Modulo Theories (SMT)solvers are fundamental to many programanalysis, verification, design and testing tools. They are a goodfit for the domain of software and hardware engineering becausethey support many domains that are commonly used by the tools.The meaning of domains are captured by theories that can beaxiomatized or supported by efficient <i>theory solvers</i>.Nevertheless, not all domains are handled by all solvers andmany domains and theories will never be native to any solver.We here explore different theories that extend MicrosoftResearch's SMT solver Z3's basicsupport. Some can be directly encoded or axiomatized,others make use of user theory plug-ins.Plug-ins are a powerful way for tools to supply their custom domains.

scholarly journals Continuous Domains in Formal Concept Analysis*

2021 ◽  
Vol 179 (3) ◽  
pp. 295-319
Author(s):  
Longchun Wang ◽  
Lankun Guo ◽  
Qingguo Li
Keyword(s):  
Formal Concept Analysis ◽  
Concept Analysis ◽  
Continuous Functions ◽  
Formal Context ◽  
Formal Concept ◽  
Contractive Mappings ◽  
Continuous Domains ◽  
Algebraic Domains ◽  
Scott Continuous ◽  
Continuous Domain

Formal Concept Analysis (FCA) has been proven to be an effective method of restructuring complete lattices and various algebraic domains. In this paper, the notion of contractive mappings over formal contexts is proposed, which can be viewed as a generalization of interior operators on sets into the framework of FCA. Then, by considering subset-selections consistent with contractive mappings, the notions of attribute continuous formal contexts and continuous concepts are introduced. It is shown that the set of continuous concepts of an attribute continuous formal context forms a continuous domain, and every continuous domain can be restructured in this way. Moreover, the notion of F-morphisms is identified to produce a category equivalent to that of continuous domains with Scott continuous functions. The paper also investigates the representations of various subclasses of continuous domains including algebraic domains and stably continuous semilattices.

Sign in / Sign up

Export Citation Format

Share Document