We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world (...) and a formula. We present a framework for local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and divide-and-conquer algorithms. (shrink)

The distributed temporal logic (DTL) is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system’s agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. Different versions of DTL have been provided over the years for a number of different applications, reflecting different perspectives on how non-local information can be accessed by each agent. In this paper, we propose an automata-theoretic model (...) checking algorithm for DTL. To this end, we propose a notion of distributed transition system that will be used to specify the system to be verified. The properties that the system should meet are specified in DTL. In order to capture the models of these properties, we propose the notions of generalized distributed Büchi automaton and of distributed Büchi automaton. With these concepts, we are able to adapt results from automata-theoretic approaches to model checking in LTL to the distributed case. (shrink)

This paper concerns model-checking of fragments and extensions of CTL* on infinite-state Presburger counter systems, where the states are vectors of integers and the transitions are determined by means of relations definable within Presburger arithmetic. In general, reachability properties of counter systems are undecidable, but we have identified a natural class of admissible counter systems (ACS) for which we show that the quantification over paths in CTL* can be simulated by quantification over tuples of natural numbers, eventually allowing (...) translation of the whole Presburger-CTL* into Presburger arithmetic, thereby enabling effective model checking. We provide evidence that our results are close to optimal with respect to the class of counter systems described above. (shrink)

Most model checking techniques for security protocols make a number of simplifying assumptions on the protocol and/or on its execution environment that greatly complicate or even prevent their applicability in some important cases. For instance, most techniques assume that communication between honest principals is controlled by a Dolev-Yao intruder, i.e. a malicious agent capable to overhear, divert, and fake messages. Yet we might be interested in establishing the security of a protocol that relies on a less unsecure channel (...) (e.g. a confidential channel provided by some other protocol sitting lower in the protocol stack). In this paper we propose a general model for security protocols based on the set-rewriting formalism that, coupled with the use of LTL, allows for the specification of assumptions on principals and communication channels as well as of complex security properties that are normally not handled by state-of-the-art security protocol analysers. By using our approach we have been able to formalise all the assumptions required by the ASW protocol for optimistic fair exchange and some of its key security properties. Besides the previously reported attacks on the protocol, we report a new attack on a patched version of the protocol. (shrink)

Model checking is a widely used technique that aids in the designand debugging of reactive systems. This paper gives an overview onthe theory and algorithms used for model checking, with a biastowards automata-theoretic approaches and linear-time temporallogic. We also describe elementary abstraction techniques useful forlarge systems that cannot be directly handled by model checking.

Models treating the simple properties of social groups have a common shortcoming. Typically, they focus on the local properties of group members and the features of the world with which group members interact. I consider economic models of bureaucratic corruption, to show that (a) simple properties of groups are often constituted by the properties of the wider population, and (b) even sophisticated models are commonly inadequate to account for many simple social properties. Adequate models and social policies must treat (...) certain factors that are not local to individual members of the group, even if those factors are not causally connected to those individuals. Key Words: individualism • corruption • supervenience • model • cause. (shrink)

This paper constructs two classes of models for the quantum correlation experiments used to test the Bell-type inequalities, synchronization models and prism models. Both classes employ deterministic hidden variables, satisfy the causal requirements of physical locality, and yield precisely the quantum mechanical statistics. In the synchronization models, the joint probabilities, for each emission, do not factor in the manner of stochastic independence, showing that such factorizability is not required for locality. In the prism models the observables are not random variables (...) over a common space; hence these models throw into question the entire random variables idiom of the literature. Both classes of models appear to be testable. (shrink)

I introduce a distinction between general and local model-data symbiosis and offer three examples of local symbiosis in the fields of meteorology and climate science. Local model-data symbiosis ref...

Arguments are provided for the reality of the quantum vacuum fields. A polarization correlation experiment with two maximally entangled photons created by spontaneous parametric down-conversion is studied in the Weyl–Wigner formalism, that reproduces the quantum predictions. An interpretation is proposed in terms of stochastic processes assuming that the quantum vacuum fields are real. This proves that local realism is compatible with a violation of Bell inequalities, thus rebutting the claim that it has been refuted by experiments. Entanglement appears as (...) a correlation between fluctuations of a signal field and vacuum fields. (shrink)

We consider Guttman scales both from an algebraic and a statistical point of view. We present a duality between a class of algebras and Guttman scalable response structures, and show that the index of reproducibility is not always a reliable indicator for the Guttman scalability of a data set. Furthermore, we present a model checking procedure, and close with an example.

Model checking, a prominent formal method used to predict and explain the behaviour of software and hardware systems, is examined on the basis of reflective work in the philosophy of science concerning the ontology of scientific theories and model-based reasoning. The empirical theories of computational systems that model checking techniques enable one to build are identified, in the light of the semantic conception of scientific theories, with families of models that are interconnected by simulation relations. (...) And the mappings between these scientific theories and computational systems in their scope are analyzed in terms of suitable specializations of the notions of model of experiment and model of data. Furthermore, the extensively mechanized character of model-based reasoning in model checking is highlighted by a comparison with proof procedures adopted by other formal methods in computer science. Finally, potential epistemic benefits flowing from the application of model checking in other areas of scientific inquiry are emphasized in the context of computer simulation studies of biological information processing. (shrink)

We investigate a SAT-based bounded model checking method for EMTLK that is interpreted over timed models generated by timed interpreted systems. In particular, we translate the existential model checking problem for EMTLK to the existential model checking problem for a variant of linear temporal logic, and we provide a SAT-based BMC technique for HLTLK. We evaluated the performance of our BMC by means of a variant of a timed generic pipeline paradigm scenario and a (...) timed train controller system. (shrink)

L. Vervoort claims to have found a model which “can violate the Bell inequality and reproduce the quantum statistics, even if it is based on local dynamics only”. This claim is false. The proposed model contains global elements. The physics behind the model is local, but would not allow the explanation of violations of Bell inequalities for space-like separated events, if superluminal causal influences are forbidden. To use it for this purpose, one has to introduce (...) a preferred frame where information can be send faster than light. As a cause of the misunderstanding we identify the unfortunate convention to use “local” as a synonym for Einstein-local, so that theories which are local in every physically relevant sense have to be named “non-local”, and argue that this convention should be abandoned. (shrink)

It is known that the full computation-tree logic CTL * is an important base logic for model checking. The bisimulation theorem for CTL* is known to be useful for abstraction in model checking. In this paper, the bisimulation theorems for two paraconsistent four-valued extensions 4CTL* and 4LCTL* of CTL* are shown, and a translation from 4CTL* into CTL* is presented. By using 4CTL* and 4LCTL*, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model (...) class='Hi'>checking framework. (shrink)

We present a variant of ATL with incomplete information which includes the distributed knowledge operators corresponding to synchronous action and perfect recall. The cooperation modalities assume the use the distributed knowledge of coalitions and accordingly refer to perfect recall incomplete information strategies. We propose a model-checking algorithm for the logic. It is based on techniques for games with imperfect information and partially observable objectives, and involves deciding emptiness for automata on infinite trees. We also propose an axiomatic system (...) and prove its completeness for a rather expressive subset. As for the constructs left outside this completely axiomatised subset, we present axioms by which they can be defined in the subset on the class of models in which every state has finitely many successors and give a complete axiomatisation for a “flat” subset of the logic with these constructs included. (shrink)

We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2EXPTIME, thus 2EXPTIME-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2EXPTIME-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem (...) that we introduce specifically for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2EXPTIME. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines. (shrink)

There is considerable confusion about the role of p-values in statistical model checking. To clarify that point, I introduce the distinction between measures of surprise and measures of evidence which come with different epistemological functions. I argue that p-values, often understood as measures of evidence against a null model, do not count as proper measures of evidence and are closer to measures of surprise. Finally, I sketch how the problem of old evidence may be tackled by acknowledging (...) the epistemic role of surprise indices. (shrink)

This paper deals with the problem of verification of game-like structures by means of symbolic model checking. Alternating-time Temporal Epistemic Logic (ATEL) is used for expressing properties of multi-agent systems represented by alternating epistemic temporal systems as well as concurrent epistemic game structures. Unbounded model checking (a SAT based technique) is applied for the first time to verification of ATEL. An example is given to show an application of the technique.

It is known that the full computation-tree logic CTL∗is an important base logic for model checking. The bisimulation theorem for CTL∗is known to be useful for abstraction in model checking. In this paper, thebisimulation theorems for two paraconsistent four-valued extensions 4CTL∗and 4LCTL∗of CTL∗are shown, and a translation from 4CTL∗into CTL∗ispresented. By using 4CTL∗and 4LCTL∗, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.

Software-controlled bots, also called social bots, are computer programs that act like human users on social media platforms. Recent work on detection of social bots is dominated by machine learning approaches. In this paper we explore bot detection as a model checking problem. We introduce Temporal Network Logic which we use to specify social networks where agents can post and follow each other. In this logic we formalize different types of social bot behavior. These are formulas that are (...) satisfied in a model of a network with bots. We provide a simple algorithm to extract a logical model from a real-life social network. We show that we can reduce TNL to a fragment of linear temporal logic with past and use this to establish the computational efficiency of model checking for social bot detection. (shrink)

We introduce a principle of local collection for compositional truth predicates and show that it is arithmetically conservative over the classically compositional theory of truth. This axiom states that upon restriction to formulae of any syntactic complexity, the resulting predicate satisfies full collection. In particular, arguments using collection for the truth predicate applied to sentences occurring in any given (code of a) proof do not suffice to show that the conclusion of that proof is true, in stark contrast to (...) the case of the induction scheme. We analyse various further results concerning end-extensions of models of compositional truth and the collection scheme for the compositional truth predicate. (shrink)

Recent work by Wan and McLean has shown that all quantum measurements may be reduced to local position measurements. Using an array of particle detectors as the measuring apparatus we show how a model employing superselection rules and unitary evolution leads to a single detector triggering in each act of measurement. We also present an explicit model of particle detection as a unitary ionization process producing a single ion in the detector, subsequent amplification of which to the (...) visible can be described adequately in classical terms. (shrink)

We construct a local \-epistemic hidden-variable model of Bell correlations by a retrocausal adaptation of the originally superdeterministic model given by Brans. In our model, for a pair of particles the joint quantum state \\rangle \) as determined by preparation is epistemic. The model also assigns to the pair of particles a factorisable joint quantum state \\rangle \) which is different from the prepared quantum state \\rangle \) and has an ontic status. The ontic state (...) of a single particle consists of two parts. First, a single particle ontic quantum state \|i\rangle \), where \\) is a 3-space wavepacket and \ is a spin eigenstate of the future measurement setting. Second, a particle position in 3-space \\), which evolves via a de Broglie–Bohm type guidance equation with the 3-space wavepacket \\) acting as a local pilot wave. The joint ontic quantum state \\rangle \) fixes the measurement outcomes deterministically whereas the prepared quantum state \\rangle \) determines the distribution of the \\rangle \)’s over an ensemble. Both \\rangle \) and \\rangle \) evolve via the Schrodinger equation. Our model exactly reproduces the Bell correlations for any pair of measurement settings. We also consider ‘non-equilibrium’ extensions of the model with an arbitrary distribution of hidden variables. We show that, in non-equilibrium, the model generally violates no-signalling constraints while remaining local with respect to both ontology and interaction between particles. We argue that our model shares some structural similarities with the modal class of interpretations of quantum mechanics. (shrink)

Let α be any countable admissible ordinal greater than ω. There is a transitive set A such that A is admissible, locally countable, On A = α, and A satisfies Σ 1 -separation. In fact, if B is any nonstandard model of $KP + \forall x \subseteq \omega$ (the hyperjump of x exists), the ordinal standard part of B is greater than ω, and every standard ordinal in B is countable in B, then HC B ∩ (standard part of (...) B) satisfies Σ 1 -separation. (shrink)