Search

We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the description of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. For parametric systems specified in this logic, we show that decision problems such as reaching deadlock or violating critical section are undecidable, in general. Despite this negative result, we provide for these decision problems practical semi-algorithms relying on the automatic synthesis of structural invariants allowing the proof of general safety properties. The invariants are defined using the WS κ S fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection, thus reducing a verification problem to checking satisfiability of a WS κ S formula. • We introduce a logic-based language for describing sets of configurations of parameterized distributed systems. • The language uses predicate symbols to hierarchically decompose the system architecture into specific patterns. • We address a parametric safety problem i.e., checking that reachable configurations stay clear of error configurations. • We show that deadlock freedom and critical section violation problems are undecidable, even for simple architectures. • We develop a verification method that synthesizes parametric invariants described using a decidable fragment of MSO. [ABSTRACT FROM AUTHOR]

Owing to the massive growth in the storage demands of big data, cloud storage systems emerge at a historic moment, among which block-based cloud storage systems (BCSSs) are typical. Compared with traditional storage systems, BCSSs have many advantages, such as higher capacity, lower cost, and better scalability. BCSSs are also much more complex and error prone than traditional systems, and therefore, their reliability is a significant concern. Correctness is the most basic requirement for reliability. Therefore, it is of great significance to study BCSS program correctness verification to establish the theoretical basis for cloud storage systems. In this paper, we propose a novel framework based on separation logic (SL) to verify the correctness of BCSS management programs. We first construct a two-tier heap structure as the formal model of the storage architecture for BCSSs and present a modelling language based on this structure to describe the program execution. We then define assertion pairs to describe the properties of the two-tier structure. The two components of an assertion pair affect each other, producing several interesting properties. Finally, we propose a Hoare-style proof system to reason about BCSS programs and establish its soundness. We also demonstrate our proof system's uniqueness, usability, and scalability by verifying several real-world BCSS sample programs. In summary, this work presents a systematic approach that can be used to effectively solve BCSS program verification problems, and provides an SL-based logical modelling strategy, specifically to build its consistency with the actual behaviour of BCSSs. • Two-tier heap structure as a formal model of a block-based cloud storage system. • Separation logic-based assertion language with several new operators and connectives. • Hoare-style proof system to reason about BCSS management programs and its soundness. • Methods for formulation of specification rules to make them concise and effective. [ABSTRACT FROM AUTHOR]

Fidelity is one of the most widely used quantities in quantum information that measures the distance of two quantum states through a noisy channel, a kind of quantum operations. In this paper, we consider the model of quantum Markov chain (QMC), in which transitions are weighted by super-operators to characterize quantum operations and the initial quantum state is left parametric. A quantum analogy of probabilistic computation tree logic, called QCTL, is introduced to take into account fidelity, instead of probability measure, over QMC. The key to the model checking problem lies in computing the fidelity of the super-operator valued measure specified by a path formula in QCTL. It is minimized over all initial quantum states, which is intended for analyzing the system performance in the worst case. We achieve it by a reduction to quantifier elimination in the existential theory of the reals. The method is absolutely exact, so that model checking QCTL formulas against QMCs is proved to be decidable in exponential time. [ABSTRACT FROM AUTHOR]

We prove that branching-time temporal logics CTL and CT L ⁎ are polynomial-time embeddable into their single-variable fragments. It follows that satisfiability for CTL and CT L ⁎ , and therefore also for alternating-time temporal logics ATL and ATL ⁎ , in languages with one propositional variable is as algorithmically hard as satisfiability for the full logic: EXPTIME-complete for CTL and ATL , and 2EXPTIME-complete for CT L ⁎ and ATL ⁎. We discuss applicability of the technique used in the proofs to other modal and temporal logics, including propositional dynamic, epistemic, and temporal-epistemic logics, as well as many-dimensional and first-order modal and temporal logics. [ABSTRACT FROM AUTHOR]

We provide a behavioural logic for configuration structures, a model due to van Glabbeek and Plotkin which generalises the families of (finite) configurations of event structures. The logic is a conservative extension of a logic provided by Baldan and Crafa for prime event structures. We show that logical equivalence can be characterized as a form of hereditary history preserving bisimilarity. We compare such a notion of bisimilarity with an equivalence proposed by van Glabbeek in the setting of higher-dimensional automata, showing that, in general, it is finer, while the two notions coincide in the framework of general event structures. Finally, we explore how to restrict the general logic to capture a notion of history preserving bisimilarity. [ABSTRACT FROM AUTHOR]

• We study the logical and extensional representations of feature models. • We study the logical and extensional representations of attributed feature models. • We investigate the algebraic properties of operations and relations on the extensional representations of both models. • We identify the logical counterpart of the above relations and operations for both basic and attributed feature models. • We show that these operations and relations have meaning in lattices. Software-intensive systems can have thousands of interdependent configuration options across different subsystems. Feature models (FMs) allow designers to organize the configuration space by describing configuration options using interdependent features: a feature is a name representing some functionality and each software variant is identified by a set of features. Attributed feature models (AFMs) extend FMs to describe the, possibly constrained, choice of a value from domains such as integers or strings: each attribute is associated to one feature, and when the feature is selected then the attribute brings some additional information relative to the selected features. Different representations of FMs and AFMs have been proposed in the literature. In this paper we focus on the logical representation (which works well in practice) and the extensional representation (which has been recently shown well suited for theoretical investigations). We provide an algebraic and a logical characterization of operations and relations on FMs and AFMs, and we formalize the connection between the two characterizations as monomorphisms from lattices of logical FMs and AFMs to lattices of extensional FMs and AFMs, respectively. This formalization sheds new light on the correspondence between the algebraic and logical characterizations of operations and relations for FMs and AFMs. It aims to foster the development of a formal framework for supporting practical exploitation of future theoretical developments on FMs, AFMs and multi software product lines. [ABSTRACT FROM AUTHOR]

• We connect two different fields: differential program semantics and incremental computing. • Program distance is increasingly important for software analysis. • Differential logical relations are a new technique that measures the distance between programs as a third program. • Program derivates are used as a way to achieve incremental computation in higher-order languages. • Program derivates are canonical self-distances and differential logical relations can be used in incremental computing. We study the deep relation existing between differential logical relations and incremental computing by showing how self-differences in the former precisely correspond to derivatives in the latter. The byproduct of such a relationship is twofold: on the one hand, we show how differential logical relations can be seen as a powerful meta-theoretical tool in the analysis of incremental computations, enabling an easy proof of soundness of differentiation. On the other hand, we generalize differential logical relations so as to be able to interpret full recursion, something not possible in the original system. [ABSTRACT FROM AUTHOR]

In the area of Natural Computing, Reaction Systems (RSs) are a qualitative abstraction inspired by the functioning of living cells, suitable to model the main mechanisms of biochemical reactions. RSs interact with a context, and pose challenges for modularity, compositionality, extendibility and behavioural equivalence. In this paper we define a modular encoding of RSs as processes in the chained Core Network Algebra (cCNA), which is a new variant of the link-calculus. The encoding represents the behaviour of each entity separately and preserves faithfully their features, and we prove its correctness and completeness. Our encoding provides a Labelled Transition System (LTS) semantics for RSs. Based on the LTS semantics, we adapt the classical notion of bisimulation to define a novel equivalence, called bio-similarity, for studying properties of RSs. In particular, we define a new assertion language based on regular expressions, which allows us to specify the properties of interest, and use it to extend Hennessy-Milner logic to our setting. We prove that our bio-similarity relation and the logical equivalence, that are defined parametrically on some assertion of interest, coincide. Finally, we claim that our encoding contributes to increase the expressiveness of RSs, by exploiting the interaction among different RSs. [ABSTRACT FROM AUTHOR]

AGM's belief revision is one of the main paradigms in the study of belief change operations. Recently, several logics for belief and information change have been proposed in the literature and used to encode belief change operations in rich and expressive semantic frameworks. While the connections of AGM-like operations and their encoding in dynamic doxastic logics have been studied before by the work of Segerberg, most works on the area of Dynamic Epistemic Logics (DEL) have not, to our knowledge, attempted to use those logics as tools to investigate mathematical properties of belief change operators. This work investigates how Dynamic Preference Logic, a logic in the DEL family, can be used to study properties of dynamic belief change operators, focusing on well-known postulates of iterated belief change. • Iterated belief change postulates can be encoded within Dynamic Preference Logic. • These postulates are dependent Grove's models and can be generalized in our logic. • With the resulting axioms, we can obtain proof systems for new dynamic logics. [ABSTRACT FROM AUTHOR]

• Unified Temporal Logic (UTL) is proposed which combines the characteristics of standard Linear Temporal Logic and Propositional Projection Temporal Logic. • The syntax and semantics of UTL are defined. • Logic laws in UTL are explored and some of them are semantically proved in detail. • The normal forms of UTL formulas are defined. It is also proved that each UTL formula can be equivalently transformed into a normal form. • A practical example of an elevator control system is given to show how to describe temporal properties with UTL. This paper proposes a new temporal logic named Unified Temporal Logic (UTL). First, the syntax and semantics of UTL are inductively defined. Further, logic laws in UTL are formalized and proved. Moreover, the normal forms of UTL formulas are defined and proved. To illustrate how to describe properties with UTL, an example of an elevator control system is given. In general, UTL combines the characteristics of Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). So properties involving the "until" construct in LTL and the "chop" construct in PPTL can easily be represented in UTL. In addition, both finite and infinite models (intervals) are supported. With UTL, we are able to specify and verify some practical properties which cannot easily be formalized in LTL and PPTL. [ABSTRACT FROM AUTHOR]

This paper proposes a dynamic approach of specification mining for Propositional Projection Temporal Logic (PPTL). To this end, a pattern library is built to collect some common temporal relation among events. Further, several algorithms of specification mining for PPTL are designed. With our approach, PPTL specifications are mined from a trace set of a target program by using patterns in the library. In addition, a specification mining tool PPTLMiner supporting this approach is developed. In practice, given a trace set and user selected patterns, PPTLMiner can capture PPTL specifications of target programs. • A PPTL specification mining approach is proposed. • A tool PPTLMiner is developed. • An open and user-editable pattern library is built. [ABSTRACT FROM AUTHOR]

• A set of theories is presented over multi-matching nested relations, including words, expressions and automata. • A new temporal logic of multi-matching nested calls and returns (MNCARET) is proposed. • An approach to model check MNCARET formulas for the MNTA model is presented. Multi-matching nested relation consists of a sequence of linearly ordered positions, call , internal , and return , augmented with one-to-one, one-to-n or n-to-one matching nested edges from call to return. For clarity, inner-call and inner-return are defined in n-to-one and one-to-n matching nested relations respectively. After word encoding by introducing tagged letters, Multi-matching Nested Words (MNWs) are obtained over a tagged alphabet. Then Multi-matching Nested Expression (MNE) and Multi-matching Nested Traceable Automaton (MNTA) are defined over MNWs. The closure properties of languages over MNWs are studied, including union, intersection, concatenation, Kleene-* and complementation. Moreover, nondeterministic MNTAs are as expressive as deterministic ones. Further, a transformation method from MNTAs to MNEs is proposed, where three kinds of labeled arcs are created for different transitions in order for the specific merging strategies. To specify the requirements of multi-matching nested calls and returns , we propose a temporal logic of Multi-matching Nested CAlls and RETurns (MNCARET). The abstract and matched-abstract versions of modalities are considered. For example, abstract-next operator allows a path to jump from a call to the first matched non- internal , which is the inner-call , inner-return or return , in a one-to-n or n-to-one matching relation while matched-abstract-next operator from a call directly to the matched return. We also present an approach to model check MNCARET formulas for the MNTA model, a subset of pushdown automata. This problem is reduced to the emptiness problem of Büchi MNTAs. [ABSTRACT FROM AUTHOR]

This paper studies the linear time-branching time spectrum of equivalences for a subclass of interactive Markov chains (IMCs) that are not subject to any further synchronization. This subclass of IMCs is known as closed IMCs. We define several variants of trace equivalence by performing button pushing experiments on stochastic trace machines. We establish the relation between these equivalences and also compare them with bisimulation for closed IMCs. Next, we define several variants of stutter trace equivalence for closed IMCs. We perform button pushing experiments with stutter insensitive stochastic trace machines to obtain these equivalences. We investigate the relationship among these stutter trace equivalences and also compare them with weak bisimulation for closed IMCs. We discuss the relation between several strong and weak trace equivalences defined in this paper. Next, we use these results to sketch the linear time-branching time spectrum of equivalences for IMCs. Finally, we prove that maximum and minimum probabilities of satisfying properties specified using metric temporal logic (MTL) formulas are preserved under some of these trace and stutter trace equivalences. [ABSTRACT FROM AUTHOR]

System I is a proof language for a fragment of propositional logic where isomorphic propositions, such as A ∧ B and B ∧ A , or A ⇒ (B ∧ C) and (A ⇒ B) ∧ (A ⇒ C) are made equal. System I enjoys the strong normalization property. This is sufficient to prove the existence of empty types, but not to prove the introduction property (every closed term in normal form is an introduction). Moreover, a severe restriction had to be made on the types of the variables in order to obtain the existence of empty types. We show here that adding η -expansion rules to System I permits to drop this restriction, and yields a strongly normalizing calculus which enjoys the full introduction property. [ABSTRACT FROM AUTHOR]

In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of temporal logics to suitable subclasses of context-free languages and appropriate extensions of temporal logics. To the best of our knowledge such attempts only covered structured languages , i.e. languages whose structure is immediately "visible" in their sentences, such as tree-languages or visibly pushdown ones. In this paper we present a new temporal logic suitable to express and automatically verify properties of operator precedence languages. This "historical" language family has been recently proved to enjoy fundamental algebraic and logic properties that make it suitable for model checking applications yet breaking the barrier of visible-structure languages (in fact the original motivation of its inventor Floyd was just to support efficient parsing , i.e. building the "hidden syntax tree" of language sentences). We prove that our logic is at least as expressive as analogous logics defined for visible pushdown languages yet covering a much more powerful family; we design a procedure that, given a formula in our logic builds an automaton recognizing the sentences satisfying the formula, whose size is at most exponential in the length of the formula. Our results cover both finite and infinite string languages. [ABSTRACT FROM AUTHOR]

We introduce a formal logical language, called conditional probability logic (CPL) , which extends first-order logic and which can express probabilities, conditional probabilities and which can compare conditional probabilities. Intuitively speaking, although formal details are different, CPL can express the same kind of statements as some languages which have been considered in the artificial intelligence community. We also consider a way of making precise the notion of lifted Bayesian network , where this notion is a type of (lifted) probabilistic graphical model used in machine learning, data mining and artificial intelligence. A lifted Bayesian network (in the sense defined here) determines, in a natural way, a probability distribution on the set of all structures (in the sense of first-order logic) with a common finite domain D. Our main result (Theorem 3.14) is that for every "noncritical" CPL-formula φ (x ¯) there is a quantifier-free formula φ ⁎ (x ¯) which is "almost surely" equivalent to φ (x ¯) as the cardinality of D tends towards infinity. This is relevant for the problem of making probabilistic inferences on large domains D , because (a) the problem of evaluating, by "brute force", the probability of φ (x ¯) being true for some sequence d ¯ of elements from D has, in general, (highly) exponential time complexity in the cardinality of D , and (b) the corresponding probability for the quantifier-free φ ⁎ (x ¯) depends only on the lifted Bayesian network and not on D. Some conclusions regarding the computational complexity of finding φ ⁎ are given in Remark 3.17. The main result has two corollaries, one of which is a convergence law (and zero-one law) for noncritial CPL-formulas. [ABSTRACT FROM AUTHOR]

We present a method to extract knowledge in terms of quantifier-free sentences in disjunctive normal form from noisy samples of classified strings. We show that the problem to find such a sentence is NP-complete, and our approach for solving it is based on a reduction to the Boolean satisfiability problem. Moreover, our method bounds the number of disjuncts and the maximum number of literals per clause since sentences with few clauses and few literals per clause are easier to interpret. As the logic we are considering defines exactly the class of locally threshold testable (LTT) languages, our results can be useful in grammatical inference when the goal is to find a model of an LTT language from a sample of strings. We also use results of the Ehrenfeucht–Fraïssé game over strings in order to handle consistent and inconsistent samples of strings. [ABSTRACT FROM AUTHOR]

The decision problem for Propositional Projection Temporal Logic (PPTL) has been solved successfully, however time complexity of the procedure is increased exponentially to the length of the formula. To solve the problem, a labeled unified complete normal form is introduced as the intermediate form to rewrite a PPTL formula into its equivalent labeled normal form, based on which the labeled normal form graph is constructed, and an efficient decision procedure for PPTL is formalized with the time complexity linear to the length of the formula and the size of the power set of the atomic propositions in the formula. Besides, an example is given to show how the improved decision procedure works. [ABSTRACT FROM AUTHOR]

Theorem proving is one of the most widely used approaches to the verification of computer systems, and its theoretical basis is generally a proof system for formal derivation of logic formulas. In this paper, we propose a sound and complete proof system for Propositional Projection Temporal Logic (PPTL) with indexed expressions, which is a unified temporal logic that subsumes the well used Linear Temporal Logic (LTL). First, the syntax, semantics and logic laws of PPTL that allows indexed expressions are introduced, and the representation of LTL constructs by PPTL formulas is illustrated. Then, the proof system for the logic is presented which consists of axioms and inference rules for the derivation of both basic constructs and indexed expressions. To show the capability of the proof system, several examples of formal proofs are provided. Finally, the soundness and completeness of the proof system are demonstrated. [ABSTRACT FROM AUTHOR]

A specification given as a formula in linear temporal logic (LTL) defines a system by its set of traces. However, certain features such as information flow security constraints are rather modeled as so-called hyperproperties, which are sets of sets of traces. One logical approach to this is team logic, which is a logical framework for the specification of dependence and independence of information. LTL with team semantics has recently been discovered as a logic for hyperproperties. We study the complexity theoretic aspects of LTL with so-called synchronous team semantics and Boolean negation, and prove that both its model checking and satisfiability problems are highly undecidable, and equivalent to the decision problem of third-order arithmetic. Furthermore, we prove that this complexity already appears at small temporal depth and with only the "future" modality F. Finally, we also introduce a team-semantical generalization of stutter-invariance. [ABSTRACT FROM AUTHOR]

We consider bisimulation-invariant monadic second-order logic over various classes of finite transition systems. We present several combinatorial characterisations of when the expressive power of this fragment coincides with that of the modal μ -calculus. Using these characterisations we prove for some simple classes of transition systems that this is indeed the case. In particular, we show that, over the class of all finite transition systems with Cantor–Bendixson rank at most k , bisimulation-invariant Image 1 coincides with L μ. [ABSTRACT FROM AUTHOR]

To specify and verify the concurrent and reactive systems with the theorem proving approach, a complete axiomatization is formalized for first order projection temporal logic (PTL) with both finite and infinite time. To this end, PTL is restricted to a finite domain, and the syntax, semantics as well as the axiomatization of PTL are presented. Further, the techniques of labeled normal form and labeled normal form graph of PTL formulas are introduced respectively, with which a decision procedure for quantifier free PTL (QFPTL) formulas is given. Moreover, a generalized labeled normal form graph is defined and employed to transform a quantified PTL formula into its equivalent QFPTL formula. Finally, a decision procedure for PTL is formalized and the completeness of the axiomatic system is proved based on the decidability of PTL formulas. [ABSTRACT FROM AUTHOR]

This paper addresses the problem of verifying heap evolution properties of pointer programs. To this end, a new unified model checking approach with MSVL (Modeling, Simulation and Verification Language) and PPTLSL is presented. The former is an executable subset of PTL (Projection Temporal Logic) while the latter is an extension of PPTL (Propositional Projection Temporal Logic) with separation logic. MSVL is used to model pointer programs, and PPTLSL to specify heap evolution properties. Technically, on one hand, models of MSVL programs are characterized by Normal Form Graphs (NFGs). On the other hand, PPTLSL is equisatisfiably reduced to its subset which can reuse the decision procedure of PPTL. Our technique is able to deal with a variety of pointer structures such as linked lists and composite structures. In addition, we implement a prototype tool by using an SMT solver as the verification engine in order to demonstrate our approach. [ABSTRACT FROM AUTHOR]

A binary decision diagram (BDDs) is a compact data structure used to represent a Boolean function, which facilitates scalable constructions of Boolean functions using reversible logic gates. Motivated by the scalable synthesis approach, this paper proposes an effective scheme for transforming the BDD representation of a Boolean function into a reversible circuit composed by reversible logic elements. Unlike a logic gate, a reversible logic element carries a memory to record a finite number of states. Especially, logic circuits composed by reversible elements can operate in asynchronous mode, thereby no need of a clock signal to drive all elements operating simultaneously. [ABSTRACT FROM AUTHOR]

Temporal logic has become essential for various areas in computer science, most notably for the specification and verification of hardware and software systems. For the specification purposes rich temporal languages are required that, in particular, can express fairness constraints. For linear-time logics which deal with fairness in the linear-time setting, one-pass and two-pass tableau methods have been developed. In the repository of the CTL-type branching-time setting, the well-known logics ECTL and ECT L + were developed to explicitly deal with fairness. However, due to the syntactical restrictions, these logics can only express restricted versions of fairness. The logic CT L ⋆ , often considered as 'the full branching-time logic' overcomes these restrictions on expressing fairness. However, CT L ⋆ is extremely challenging for the application of verification techniques, and the tableau technique, in particular. For example, there is no one-pass tableau construction for CT L ⋆ , while one-pass tableau has an additional benefit enabling the formulation of dual sequent calculi that are often treated as more 'natural' being more friendly for human understanding. These two considerations lead to the following problem - are there logics that have richer expressiveness than ECT L + , allowing the formulation of a new range of fairness constraints with 'until' operator, yet 'simpler' than CT L ⋆ , and for which a one-pass tableau can be developed? Here we give a positive answer to this question, introducing a sub-logic of CT L ⋆ called ECT L # , its tree-style one-pass tableau, and an algorithm for obtaining a systematic tableau, for any given admissible branching-time formulae. We prove the termination, soundness and completeness of the method. As tree-shaped one-pass tableaux are well suited for the automation and are amenable for the implementation and for the formulation of sequent calculi. Our results also open a prospect of relevant developments of the automation and implementation of the tableau method for ECT L # , and of a dual sequent calculi. [ABSTRACT FROM AUTHOR]

In this paper, we build a logic which is named N-sequent calculus. Based on this logic, we provide two kinds of logical representations of Lawson compact algebraic L-domains: one in terms of logical algebras and the other in terms of logical syntax. The first representation takes the corresponding logical algebras as research objects. The use of prime filters achieves the connection between our logic and Lawson compact algebraic L-domains. This approach is inspired by Abramsky's SFP domain logic and the disjunctive propositional logic on algebraic L-domains introduced by Yixiang Chen and Achim Jung. However, there are essential differences between them at the morphisms part. For the second representation, we directly adopt N-sequent calculi themselves as objects instead of the logical algebras. Then we establish the category of N-sequent calculi with consequence relations equivalent to that of Lawson compact algebraic L-domains with Scott continuous maps. This demonstrates the capability of the syntax of the logic in representing domains. [ABSTRACT FROM AUTHOR]

We provide a proofs-as-concurrent-programs interpretation for a large class of intermediate logics that can be formalized by cut-free hypersequent calculi. Obtained by adding classical disjunctive tautologies to intuitionistic logic, these logics are used to type concurrent λ -calculi by Curry–Howard correspondence; each of the calculi features a specific communication mechanism, enhanced expressive power when compared to the λ -calculus, and implements forms of code mobility. We thus confirm Avron's 1991 thesis that intermediate logics formalizable by hypersequent calculi can serve as basis for concurrent λ -calculi. [ABSTRACT FROM AUTHOR]

Hybrid branching-time logics are a powerful extension of branching-time logics like CTL, CTL⁎ or even the modal μ -calculus through the addition of binders, jumps and variable tests. Their expressiveness is not restricted by bisimulation-invariance anymore. Hence, they do not retain the tree model property, and the finite model property is equally lost. Their satisfiability problems are typically undecidable, their model checking problems (on finite models) are decidable with complexities ranging from polynomial to non-elementary time. In this paper we study the expressive power of such hybrid branching-time logics. We extend the hierarchy of branching-time logics CTL, CTL+, CTL⁎ and the modal μ -calculus to their hybrid extensions. We show that most separation results can be transferred to the hybrid world, even though the required techniques become more involved. We also present collapse results for linear, tree-shaped and finite models. [ABSTRACT FROM AUTHOR]

In the last years, some extensions of ω -regular languages, namely, ωB -regular (ω -regular languages extended with boundedness), ωS -regular (ω -regular languages extended with strong unboundedness), and ωBS -regular languages (the combination of ωB - and ωS -regular ones), have been proposed in the literature. While the first two classes satisfy a generalized closure property, which states that the complement of an ωB -regular (resp., ωS -regular) language is an ωS -regular (resp., ωB -regular) one, the last class is not closed under complementation. The existence of non- ωBS -regular languages that are the complements of some ωBS -regular ones and express fairly natural asymptotic behaviors motivates the search for other significant classes of extended ω -regular languages. In this paper, we present the class of ωT -regular languages, which includes meaningful languages that are not ωBS -regular. We define this new class of languages in terms of ωT -regular expressions. Then, we introduce a new class of automata (counter-check automata) and we prove that (i) their emptiness problem is decidable in PTIME, and (ii) they are expressive enough to capture ωT -regular languages. We also provide an encoding of ωT -regular expressions into S1S + U. Finally, we investigate a stronger variant of ωT -regular languages (ω T s -regular languages). We characterize the resulting class of languages in terms of ω T s -regular expressions, and we show how to map it into a suitable class of automata, called counter-queue automata. We conclude the paper with a comparison of the expressiveness of ωT - and ω T s -regular languages and of the corresponding automata. [ABSTRACT FROM AUTHOR]

We investigate the succinctness gap between two known equally-expressive and different linear-past extensions of standard ATL ⁎ . We establish by formal non-trivial arguments that the 'memoryful' linear-past extension (the history leading to the current state is taken into account) can be exponentially more succinct than the standard 'local' linear-past extension (the history leading to the current state is forgotten). As a second contribution, we consider the ATL -like fragment, denoted ATL l p , of the known 'memoryful' linear-past extension of ATL ⁎ . We show that ATL l p is strictly more expressive than ATL , and interestingly, it can be exponentially more succinct than the more expressive logic ATL ⁎. Moreover, we prove that both satisfiability and model-checking for the logic ATL l p are Exptime -complete. [ABSTRACT FROM AUTHOR]

Several type systems have been proposed to statically control the time complexity of lambda-calculus programs and characterize complexity classes such as FPTIME or FEXPTIME. A first line of research stems from linear logic and restricted versions of its !-modality controlling duplication. An instance of this is light linear logic for polynomial time computation [5]. A second approach relies on the idea of tracking the size increase between input and output, and together with a restricted recursion scheme, to deduce time complexity bounds. This second approach is illustrated for instance by non-size-increasing types [8]. However, both approaches suffer from limitations. The first one, that of linear logic, has a limited intensional expressivity, that is to say some natural polynomial time programs are not typable. As to the second approach it is essentially linear, more precisely it does not allow for a non-linear use of functional arguments. In the present work we incorporate both approaches into a common type system, in order to overcome their respective constraints. The source language we consider is a lambda-calculus with data-types and iteration, that is to say a variant of Gödel's system T. Our goal is to design a system for this language allowing both to handle non-linear functional arguments and to keep a good intensional expressivity. We illustrate our methodology by choosing the system of elementary linear logic (ELL) and combining it with a system of linear size types. We discuss the expressivity of this new type system, called sEAL, and prove that it gives a characterization of the complexity classes FPTIME and 2k-FEXPTIME, for k ≥ 0. [ABSTRACT FROM AUTHOR]

We show how to represent polynomial time computation in an untyped version of proof-nets for elementary linear logic. This follows previous work by P. Baillot but which was developed in a typed and affine setting. We describe how these two properties can be adapted. [ABSTRACT FROM AUTHOR]

Let A be an alphabet and S P ⋄ (A) denote the class of all countable N-free partially ordered sets labeled by A , in which chains are scattered linear orderings and antichains are finite. We characterize the rational languages of S P ⋄ (A) by means of logic. We define an extension of monadic second-order logic by Presburger arithmetic, named P-MSO, such that a language L of S P ⋄ (A) is rational if and only if L is the language of a sentence of P-MSO, with effective constructions from one formalism to the other. As a corollary, the P-MSO theory of S P ⋄ (A) is decidable. [ABSTRACT FROM AUTHOR]

This paper introduces Graded Computation Tree Logic with finite path semantics (GCTL f ⁎ , for short), a variant of Computation Tree Logic CTL⁎, in which path quantifiers are interpreted over finite paths and can count the number of such paths. State formulas of GCTL f ⁎ are interpreted over Kripke structures. The syntax of GCTL f ⁎ has path quantifiers of the form E ≥ g ψ which express that there are at least g many distinct finite paths that satisfy ψ. After defining and justifying the logic GCTL f ⁎ , we solve its model checking problem and establish that its computational complexity is PSPACE-complete. Moreover, we investigate GCTL f ⁎ under the imperfect information setting. Precisely, we introduce GCTLK f ⁎ , an epistemic extension of GCTL f ⁎ and prove that the model checking problem also in this case is PSPACE-complete. [ABSTRACT FROM AUTHOR]

We consider the one-variable fragment of first-order logic extended with Presburger constraints. The logic is designed in such a way that it subsumes the previously-known fragments extended with counting, modulo counting or cardinality comparison and combines their expressive powers. We prove Image 1 -completeness of the logic by presenting an optimal algorithm for solving its finite satisfiability problem. [ABSTRACT FROM AUTHOR]

We study a variant ATL FB of the alternating-time temporal logic ATL with a non-standard, 'finitely bounded' semantics (FBS). FBS was originally defined as a game-theoretic semantics where players must commit to time limits when attempting to verify eventuality (respectively, to falsify safety) formulae. It turns out that FBS has a natural corresponding compositional semantics that essentially evaluates formulae only on finite initial segments of paths and imposes uniform bounds on all plays for the fulfilment of eventualities. The resulting version ATL FB differs in some essential features from the standard ATL, as it no longer has the finite model property, though the two logics are equivalent on finite models. We develop two tableau systems for ATL FB. The first one deals with infinite sets of formulae and may run in a transfinite sequence of steps, whereas the second one deals only with finite sets of formulae in an extended language allowing explicit symbolic indication of time limits in formulae. We prove soundness and completeness of the infinitary tableau system and prove that it is equivalent to the finitary one. We also show that the finitary tableau system provides an exponential-time decision procedure for the satisfiability problem of ATL FB and thus establishes its EXPTIME-completeness. Furthermore, we present an infinitary axiomatization for ATL FB and prove its soundness and completeness. [ABSTRACT FROM AUTHOR]

Halpern and Shoham modal logic of time intervals (HS in short) is an elegant and highly influential propositional interval-based modal logic. Its sub-propositional fragments, that is fragments obtained by restricting use of propositional connectives, and their hybrid extensions with nominals and satisfaction operators have been recently studied and successfully applied in real-world use cases. Detailed investigation of their decidability and computational complexity has been conducted, however, there has been significantly less research on their expressive power. In this paper we make a step towards filling this gap. In particular, we (1) compare classes of frames definable in full HS and in its hybrid extension, and (2) determine in which sub-propositional HS -fragments we can express the difference operator, nominals, and satisfaction operators. The obtained results enable us to classify HS , its sub-propositional fragments, and their hybrid extensions according to their expressive power. [ABSTRACT FROM AUTHOR]

In Temporal Logic (TL), a well-formed formula is generally formed by applying rules of its syntax finitely many times. However, under some circumstances, although formulas such as ones expressed by index set expressions , are constructed via applying rules of the syntax infinitely many times, they are possibly still well-formed since their equivalent concise syntax formulas can be found. With this motivation, this paper investigates the relationship between formulas specified by index set expressions and concise syntax by means of fixed-point approach. Firstly, we present two kinds of formulas, namely ⋁ i ∈ N 0 ◯ i Q and ⋁ i ∈ N 0 Q i , and prove they are indeed well-formed by proving they are equivalent to formulas ◇ Q and Q ⁎ respectively. Further, we generalize ⋁ i ∈ N 0 ◯ i Q to ⋁ i ∈ N 0 P (i) ∧ ◯ i Q and explore the least and greatest fixed-points of an abstract equation X ≡ Q ∨ P ∧ ◯ X. Based on these, some well-formed special instances of ⋁ i ∈ N 0 P (i) ∧ ◯ i Q are obtained. Besides, with the index set expression technique, we equivalently represent ' U ' (strong until) and ' W ' (weak until) constructs of propositional Linear Temporal Logic (LTL) within Propositional Projection Temporal Logic (PPTL). [ABSTRACT FROM AUTHOR]

When studying sequent calculi, proof theorists often have to prove properties about the systems, whether to show that they are "well-behaved", amenable to automated proof search, complete with respect to another system, consistent, among other reasons. These proofs usually involve many very similar cases, which leads to authors rarely writing them in full detail, only pointing to one or two more complicated cases. Moreover, the amount of details makes them more error-prone for humans. Computers, on the other hand, are very good at handling details and repetitiveness. In this work we have formalized textbook proofs of the meta-theory of sequent calculi for linear logic in Abella. Using the infrastructure developed, the proofs can be easily adapted to other substructural logics. We implemented rules as clauses in an intuitive and straightforward way, similar to logic programming, using operations on multisets for the explicit contexts. Although the proofs are quite big, they use only elementary reasoning principles, which makes the proof techniques fairly portable to other formal reasoning systems. [ABSTRACT FROM AUTHOR]

Among the very many research interests of Maurice Nivat, a special role, according to the produced literature, was played by the study of the algorithmic and combinatorial aspects of connected finite discrete sets of points called polyominoes. In particular, he addressed the problem of a faithful reconstruction of some subclasses of them by imposing convexity constraints. The present study fits in this research line, and relies on a well known algorithm that Maurice Nivat and co-authors defined 1996 for the reconstruction of hv -convex polyominoes by orthogonal projections in polynomial time. Here, we consider a hierarchy on this class of polyominoes, and we continue a longstanding research on the reconstruction of its first levels by specializing the above mentioned result. The algorithm we propose bases on the possibility of characterizing the elements of the second level of the hierarchy, by a logic formula belonging to Dual-Horn and so polynomially solvable. Some related open problems are also presented. [ABSTRACT FROM AUTHOR]

A logical theory for interface specification and verification of distributed, concurrent, interactive, real-time systems is worked out based on a semantic foundation including operational and denotational semantics. It supports a calculus for the specification and verification of concurrent interactive systems by interface assertions. Systems are composed acting concurrently and interacting via streams exchanged over their channels forming feedback loops. A denotational semantics is defined handling feedback communication by recursion and fixpoints based on strong causality and realizability instead of monotonicity. The resulting verification calculus for the specification logic is proved to be sound and relatively complete with respect to an operational semantics in terms of generalized Moore machines. Actually, two models of concurrent systems are defined, a more abstract one with communication and interaction modeled by untimed streams and a more concrete one working with timed streams. The untimed model is an abstraction of the timed model. The timed model allows expressing the laws of causality and realizability. Moreover, the timed model can be used to specify real-time properties. [ABSTRACT FROM AUTHOR]

In this paper, we study the model checking problem of pushdown systems for projection temporal logic (PTL), an interval-based temporal logic that is as expressive as the full regular languages. For this, we provide an algorithm to decide whether a pushdown system, determined by a pushdown automaton, satisfies a desired logic property, by using relevant automata notations and operations. The algorithm terminates in exponential time for normal PTL properties, i.e. properties specified as normal PTL formulas. To show the lower bound of complexity of the model checking problem, we also construct a polynomial-time reduction from the acceptance problem of a linearly bounded alternating Turing machine. As a result, the model checking problem of pushdown systems for normal PTL properties is EXPTIME-complete. [ABSTRACT FROM AUTHOR]

To specify properties of open systems with interval based temporal logics, Alternating Projection Temporal Logic (APTL) is proposed by introducing Concurrent Game Structures (CGS) to Propositional Projection Temporal Logic (PPTL). Further, examples are given to show how properties of open systems can be specified by APTL formulas. Moreover, to establish the automata based model theory for the new proposed logic, Generalized alternating Büchi automata over Concurrent Game structures (GBCGs) are defined, and a transformation from APTL formulas to GBCGs is presented. In addition, a decision procedure for checking the satisfiability of APTL formulas, and a model checking approach for APTL with Concurrent Game Structures (CGSs) being models are presented. [ABSTRACT FROM AUTHOR]

Abstract Intensional computations are those that query the internal structure of their arguments. In a higher-order setting, such queries perform program analysis. This is beyond the expressive power of traditional term rewriting systems, such as lambda-calculus or combinatory logic, as they are extensional. In such settings it has been necessary to encode or quote the program before analysis. However, there are intensional calculi, specifically confluent term rewriting systems, that can analyse higher-order programs within the calculus proper, without quotation; there are even programs that produce the Goedel numbers of their program argument. This paper summarizes the current situation. Highlights include the following observations. We have known since 2011 that the simplest intensional calculus, SF-calculus, supports arbitrary queries of closed normal forms, including equality, pattern-matching, searching and self-interpretation. Recent work, verified using the Coq proof assistant, has shown that all recursive programs can be represented as closed normal forms in SF-calculus, and even in combinatory logic. Thus, we can here deduce that SF-calculus (but not combinatory logic) can define queries of programs. These results are compatible with direct support for lambda-abstraction. Although these results conflict with the traditional understanding of expressive power of combinatory logic and λ -calculus, as developed by Church and Kleene, our recent publication has shown that their approach is compromised by its reliance on encodings. To drive the point home, this paper uses a non-standard encoding to lambda-define a trivial solution of the Halting Problem. [ABSTRACT FROM AUTHOR]

An important problem when modelling gene networks lies in the identification of parameters, even when using a discrete framework such as the one of René Thomas. We present in this article a new approach based on Hoare logic to generate constraints on parameter values. Specifications of observed behaviours play a role comparable to programs in the classical Hoare logic, and deduced weakest preconditions characterize the sets of all compatible parameterizations, expressed as constraints on parameters. Besides being natural and simple, our Hoare logic approach is remarkably powerful and, among others, it allows one to express external interventions of the biologist during experiments such as knockouts. In supplementary materials, we give a proof of soundness of our Hoare logic for gene networks as well as a proof of completeness and decidability based on the notion of the weakest precondition. [ABSTRACT FROM AUTHOR]

Some extensions of ω -regular languages have been proposed in the literature to express asymptotic properties of ω -words which are not captured by ω -regular languages. They include ωB -regular languages, that extend ω -regular languages with boundedness, ωS -regular languages, that enrich ω -regular ones with strong unboundedness, ωBS -regular languages, that combine ωB - and ωS -regular ones, and ωT -regular languages, that include meaningful languages which are not ωBS -regular. Formal definitions of extended ω -regular languages have been given in terms of both suitable classes of automata and extended ω -regular expressions, while satisfactory temporal logic counterparts are still missing. In this paper, we give a characterization of them in terms of interval temporal logics by providing an explicit encoding of expressions into formulas. [ABSTRACT FROM AUTHOR]

Non-deterministic constraint logic (NCL) is a simple model of computation based on orientations of a constraint graph with edge weights and vertex demands. NCL captures PSPACE and has been a useful tool for proving algorithmic hardness of many puzzles, games, and reconfiguration problems. In particular, its usefulness stems from the fact that it remains PSPACE -complete even under severe restrictions of the weights (e.g., only edge-weights one and two are needed) and the structure of the constraint graph (e.g., planar and/or graphs of bounded bandwidth). While such restrictions on the structure of constraint graphs do not seem to limit the expressiveness of NCL , the building blocks of the constraint graphs cannot be limited without losing expressiveness: We consider as parameters the number of weight-one edges and the number of weight-two edges of a constraint graph, as well as the number of and or or vertices of an and/or constraint graph. We show that NCL is fixed-parameter tractable (FPT) for any of these parameters. In particular, for NCL parameterized by the number of weight-one edges or the number of and vertices, we obtain a linear kernel. It follows that, in a sense, NCL as introduced by Hearn and Demaine is defined in the most economical way for the purpose of capturing PSPACE. [ABSTRACT FROM AUTHOR]

We introduce a new concept in the area of formal logic: axioms for model morphisms. We work in the setting of specification languages that define the semantics of a theory as a category of models. While it is routine to use axioms to specify the class of models of a theory, there has so far been no analogue to systematically specify the morphisms between these models. This leads to subtle problems where it is difficult to give a theory that specifies the intended model category, or where seemingly isomorphic theories actually have non-isomorphic model categories. Our morphism axioms remedy this by providing new syntax for axiomatizing and reasoning about the properties of model morphisms. Additionally, our system resolves a subtle incompatibility between theory morphisms and model morphisms: the semantics that maps theories to model categories is functorial. While this result is standard in principle, previous formulations had to restrict the allowed theory morphisms or the allowed model morphisms. Our system allows establishing the result in full generality. [ABSTRACT FROM AUTHOR]

Unified Temporal Logic (UTL) combines all characteristics of traditional Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). It can be used to describe full regular and omega-regular properties, which are often encountered in the field of formal verification. To support formal verification with UTL, this paper proposes a proof system for UTL. First, the syntax and semantics of UTL are briefly introduced. Further, axioms and inference rules are formalized. Besides, a number of theorems are derived and proved to refine the system. Moreover, the soundness and completeness of the proof system are proved in detail. To facilitate the completeness proof, some auxiliary lemmas are introduced and proved in advance. Finally, an example is given to illustrate how to use this proof system for verifying properties of a system. [ABSTRACT FROM AUTHOR]