scholarly journals Dynamic logic of parallel propositional assignments and its applications to planning

2019 ◽  
Author(s):  
Andreas Herzig ◽  
Frédéric Maris ◽  
Julien Vianey
Keyword(s):  
Model Checking ◽  
Dynamic Logic ◽  
Satisfiability Problem ◽  
Parallel Composition ◽  
Conditional Effects

We introduce a dynamic logic with parallel composition and two kinds of nondeterministic composition, exclusive and inclusive. We show PSPACE completeness of both the model checking and the satisfiability problem and apply our logic to sequential and parallel classical planning where actions have conditional effects.

scholarly journals Dynamic Logic for Data-aware Systems: Decidability Results

2017 ◽  
Author(s):  
Francesco Belardinelli ◽  
Andreas Herzig
Keyword(s):  
Model Checking ◽  
Dynamic Logic ◽  
English Auctions ◽  
First Order ◽  
Formal Framework ◽  
Data Content ◽  
Order Extension

We introduce a first-order extension of dynamic logic (FO-DL), suitable to represent and reason about the behaviour of Data-aware Systems (DaS), which are systems whose data content is explicitly exhibited in the system’s description. We illustrate the expressivity of the formal framework by modelling English auctions as DaS, and by specifying relevant properties in FO-DL. Most importantly, we develop an abstraction-based verification procedure, thus proving that the model checking problem for DaS against FO-DL is actually decidable, provided some mild assumptions on the interpretationdomain.

ACTION MACHINES: A FRAMEWORK FOR ENCODING AND COMPOSING PARTIAL BEHAVIORS

2006 ◽  
Vol 16 (05) ◽  
pp. 705-726 ◽  
Author(s):  
WOLFGANG GRIESKAMP ◽  
NICOLAS KICILLOF ◽  
NIKOLAI TILLMANN
Keyword(s):  
Model Checking ◽  
Composition Operators ◽  
Parallel Composition ◽  
Full Data ◽  
Transition Systems ◽  
Main Application ◽  
Model Based ◽  
Software Models ◽  
Model Based Testing ◽  
Testing Technology

We describe action machines, a framework for encoding and composing partial behavioral descriptions. Action machines encode behavior as a variation of labeled transition systems where the labels are observable activities of the described artifact and the states capture full data models. Labels may also have structure, and both labels and states may be partial with a symbolic representation of the unknown parts. Action machines may stem from software models or programs, and can be composed in a variety of ways to synthesize new behaviors. The composition operators described here include synchronized and interleaving parallel composition, sequential composition, and alternating simulation. We use action machines in analysis processes such as model checking and model-based testing. The current main application is in the area of model-based conformance testing, where our approach addresses practical problems users at Microsoft have in applying model-based testing technology.

scholarly journals COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS

2011 ◽  
Vol 22 (04) ◽  
pp. 801-821
Author(s):  
PIETER COLLINS ◽  
IVAN S. ZAPREEV
Keyword(s):  
Model Checking ◽  
Discrete Time ◽  
Dynamic Systems ◽  
Parallel Composition ◽  
Computable Model ◽  
Continuous Space ◽  
Büchi Automaton

In this work, we consider Discrete-Time Continuous-Space Dynamic Systems for which we study the computability of the standard semantics of CTL* (CTL, LTL) and provide a variant thereof computable in the sense of Type-2 Theory of Effectivity. In particular, we show how the computable model checking of existentially and universally quantified path formulae of LTL can be reduced to solving, respectively, repeated reachability and persistence problems on a model obtained as a parallel composition of the original one and a non-deterministic Büchi automaton corresponding to the verified LTL formula.

scholarly journals From Timed Automata to Logic - and Back

1995 ◽  
Vol 2 (2) ◽  
Author(s):  
Francois Laroussinie ◽  
Kim G. Larsen ◽  
Carsten Weise
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Finite Automata ◽  
Automatic Verification ◽  
Satisfiability Problem ◽  
Timed Automaton

One of the most successful techniques for automatic verification is that<br />of model checking. For finite automata there exist since long extremely<br />efficient model-checking algorithms, and in the last few years these algorithms have been made applicable to the verification of real-time automata using the region-techniques of Alur and Dill.<br />In this paper, we continue this transfer of existing techniques from the<br />setting of finite (untimed) automata to that of timed automata. In particular, a timed logic L is put forward, which is sufficiently expressive that we for any timed automaton may construct a single characteristic L formula uniquely characterizing the automaton up to timed bisimilarity. Also, we prove decidability of the satisfiability problem for L with respect to given bounds on the number of clocks and constants of the timed automata to be constructed. None of these results have as yet been succesfully accounted for in the presence of time.

Symbolic model checking of public announcement protocols

2019 ◽  
Vol 29 (8) ◽  
pp. 1211-1249
Author(s):  
Tristan Charrier ◽  
Sophie Pinchinat ◽  
FranÇois Schwarzentruber
Keyword(s):  
Model Checking ◽  
Dynamic Logic ◽  
Symbolic Model Checking ◽  
Kripke Models ◽  
Symbolic Model ◽  
Public Announcement ◽  
Public Announcements ◽  
Protocol Logic

Abstract We study the symbolic model checking problem against public announcement protocol logic (PAPL), featuring protocols with public announcements, arbitrary public announcements and group announcements. Technically, symbolic models are Kripke models whose accessibility relations are presented as programs described in a dynamic logic style with propositional assignments. We highlight the relevance of such symbolic models and show that the symbolic model checking problem against PAPL is A$_{\textrm{pol}}$Exptime-complete as soon as announcement protocols allow for either arbitrary announcements or iteration of public announcements. However, when both options are discarded, the complexity drops to Pspace-complete.

scholarly journals LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems

10.29007/wpg3 ◽  
2018 ◽  
Author(s):  
Rachel Faran ◽  
Orna Kupferman
Keyword(s):  
Model Checking ◽  
Blow Up ◽  
Satisfiability Problem ◽  
Theoretic Approach ◽  
Hierarchical Systems ◽  
Infinite Domain ◽  
Composite Systems ◽  
System A ◽  
Computational Bottleneck ◽  
Naive Model

The computational bottleneck in model-checking applications is the blow-up involved in the translation of systems to their mathematical model. This blow up is especially painful in systems with variables over an infinite domain, and in composite systems described by means of their underlying components. We introduce and study linear temporal logic with arithmetic (LTLA, for short), where formulas include variables that take values in Z, and in which linear arithmetic over these values is supported. We develop an automata-theoretic approach for reasoning about LTLA formulas and use it in order to solve, in PSPACE, the satisfiability problem for the existential fragment of LTLA and the model-checking problem for its universal fragment. We show that these results are tight, as a single universally- quantified variable makes the satisfiability problem for LTLA undecidable.In addition to reasoning about systems with variables over Z, we suggest applications of LTLA in reasoning about hierarchical systems, which consist of subsystems that can call each other in a hierarchical manner. We use the values in Z in order to describe the nesting depth of components in the system. A naive model-checking algorithm for hierarchical systems flattens them, which involves an exponential blow up. We suggest a model-checking algorithm that avoids the flattening and avoids a blow up in the number of components.

scholarly journals Compositional and Symbolic Model-Checking of Real-Time Systems

1996 ◽  
Vol 3 (59) ◽  
Author(s):  
Kim G. Larsen ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Symbolic Model Checking ◽  
Automatic Verification ◽  
Parallel Composition ◽  
Real Time Systems ◽  
Symbolic Model ◽  
Verification Tools ◽  
State Region ◽  
Time Systems

Efficient automatic model-checking algorithms for<br />real-time systems have been obtained in recent years<br />based on the state-region graph technique of Alur,<br />Courcoubetis and Dill. However, these algorithms are<br />faced with two potential types of explosion arising from<br />parallel composition: explosion in the space of control<br />nodes, and explosion in the region space over clock variables.<br />In this paper we attack these explosion problems by<br />developing and combining compositional and symbolic<br />model-checking techniques. The presented techniques<br />provide the foundation for a new automatic verification<br />tool Uppaal. Experimental results indicate that<br />Uppaal performs time- and space-wise favorably compared<br />with other real-time verification tools.

scholarly journals The Ceteris Paribus Structure of Logics of Game Forms (Extended Abstract)

2017 ◽  
Author(s):  
Davide Grossi ◽  
Emiliano Lorini ◽  
François Schwarzentruber
Keyword(s):  
Normal Form ◽  
Dynamic Logic ◽  
Satisfiability Problem ◽  
Ceteris Paribus ◽  
Coalition Logic ◽  
Polynomial Reduction ◽  
Complexity Result ◽  
Game Forms

We present a simple Ceteris Paribus Logic (CP) and study its relationship with existing logics that deal with the representation of choice and power in games in normal form including atemporal STIT, Coalition Logic of Propositional Control (CL-PC) and Dynamic Logic of Propositional Assignments (DL-PA). Thanks to the polynomial reduction of the satisfiability problem for atemporal STIT in the satisfiability problem for CP, we obtain a complexity result for the latter problem.

scholarly journals Parameterised complexity of model checking and satisfiability in propositional dependence logic

2021 ◽  
Author(s):  
Yasir Mahmood ◽  
Arne Meier
Keyword(s):  
Model Checking ◽  
Decision Problems ◽  
Satisfiability Problem ◽  
Team Size ◽  
Dependence Logic ◽  
Fixed Parameter Tractable ◽  
Size Number ◽  
Completeness Result ◽  
Fixed Parameter ◽  
The Subject

AbstractDependence Logic was introduced by Jouko Väänänen in 2007. We study a propositional variant of this logic (PDL) and investigate a variety of parameterisations with respect to central decision problems. The model checking problem (MC) of PDL is NP-complete (Ebbing and Lohmann, SOFSEM 2012). The subject of this research is to identify a list of parameterisations (formula-size, formula-depth, treewidth, team-size, number of variables) under which MC becomes fixed-parameter tractable. Furthermore, we show that the number of disjunctions or the arity of dependence atoms (dep-arity) as a parameter both yield a paraNP-completeness result. Then, we consider the satisfiability problem (SAT) which classically is known to be NP-complete as well (Lohmann and Vollmer, Studia Logica 2013). There we are presenting a different picture: under team-size, or dep-arity SAT is paraNP-complete whereas under all other mentioned parameters the problem is FPT. Finally, we introduce a variant of the satisfiability problem, asking for a team of a given size, and show for this problem an almost complete picture.

Sign in / Sign up

Export Citation Format

Share Document