The pi-calculus [61] is one the most influential formalisms for modelling and analyzing the behaviour of concurrent systems. This calculus provides a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. For example, the parallel composition term P | Q, which is built from the terms P and Q, represents the process that results from the parallel execution of the processes P and Q. Similarly, the restriction (v x)P represents a process P with local resource x. The replication !P can be thought of as abbreviating the parallel composition P | P | . . . of an unbounded number of P processes. As for other language-based formalisms (e.g., logic, formal grammars and the pi-calculus) a fundamental part of the research in process calculi involves the study of the expressiveness of fragments or variants of a given process calculus. In this dissertation we shall study the expressiveness of some variants of the pi-calculus focusing on the role of the terms used to represent local and infinite behaviour, namely restriction and replication. The first part of this dissertation is devoted to the expressiveness of the zero-adic variant of the (polyadic) pi-calculus, i.e., CCS with replication (CCS!) [21]. Busi et al [22] show that CCS! is Turing powerful [22]. The result is obtained by encoding Random Access Machines (RAMs) in CCS!. The encoding is said to be non-faithful because it may move from a state which can lead to termination into a divergent one which do not correspond to any configuration of the encoded RAM. I.e., the encoding is not termination preserving. In this dissertation we shall study the existence of faithful encodings into CCS! of models of computability strictly less expressive than Turing Machines. Namely, grammars of Types 1 (Context Sensitive Languages), 2 (Context Free Languages) and 3 (Regular Languages) in the Chomsky Hierarchy. We provide faithful encodings of Type 3 grammars. We show that it is impossible to provide a faithful encoding of Type 2 grammars and that termination-preserving CCS! processes can generate languages which are not Type 2. We finally conjecture that the languages generated by termination-preserving CCS! processes are Type 1 . We also observe that the encoding of RAMs [22] and several encoding of Turing-powerful formalisms in pi-calculus variants may generate an unbounded number of restrictions during the simulation of a given machine. This unboundedness arises from having restrictions under the scope of replication (or recursion) as in e.g., !(v x)P or μX.(v x)(P | X). This suggests that such an interplay between these operators is fundamental for Turing completeness. We shall also study the expressive power of restriction and its interplay with replication. We do this by considering several syntactic variants of CCS! which differ from each other in the use of restriction with respect to replication. We consider three syntactic variations of CCS! which do not allow the generation of unbounded number of restrictions: C2 is the fragment of CCS! not allowing restrictions under the scope of a replication, C3 is the restriction-free fragment of CCS!. The third variant is C4 which extends C2 with Phillips' priority guards [76]. We shall show that the use of an unboundedly many restrictions in CCS! is necessary for obtaining Turing expressiveness in the sense of Busi et al [22]. We do this by showing that there is no encoding of RAMs into C2 which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS! into C2 nor from C2 into C3. Thus up to failures equivalence, we cannot encode a process with an unbounded number of restrictions into one with a bounded number of restrictions, nor one with a bounded number of restrictions into a restriction-free process. As lemmata for the above results we prove that convergence is decidable for C2 and that language equivalence is decidable for C3 but undecidable for C2. As corollary it follows that convergence is decidable for restriction-free CCS. Finally, we show the expressive power of priorities by providing a faithful encoding of RAMs in C4 thus bearing witness to the expressive power of Phillips' priority guards [76]. The second part of this dissertation is devoted to expressiveness of the asynchronous monadic pi-calculus, A [15, 47]. In [70] the authors studied the expressivenessn of persistence in Api [15, 47] wrt weak barbed congruence. The study is incomplete because it ignores divergence. We shall present an expressiveness study of persistence in Api wrt De Nicola and Hennessy's testing scenario which is sensitive to divergence. Following [70],,we consider Api and three sub-languages of it, each capturing one source of persistence: the persistent-input Api-calculus (PIA), the persistent-output Api-calculus (POA) and the persistent Api-calculus (PA). In [70] the authors showed encodings from Api into the semi-persistent calculi (i.e., POA and PIA) correct wrt weak barbed congruence. We show that, under some general conditions related to compositionality of the encoding and preservation of the infinite behaviour, there cannot be an encoding from Api into a (semi)-persistent calculus preserving the must testing semantics. We also prove that convergence and divergence are decidable for POA (and PA). As a consequence there is no encoding preserving and reflecting divergence or convergence from Api into POA (and PA). This study fills a gap on the expressiveness study of persistence in A in [70].

In 1912 Axel Thue sparked the study of combinatorics on words when he showed that the Thue-Morse sequence contains no overlaps, that is, factors of the form ayaya. Since then many interesting properties of sequences began to be discovered and studied. In this thesis, we consider a class of infinite sequences generated by automata, called the k-automatic sequences. In particular, we present a logical theory in which many properties of k-automatic sequences can be expressed as predicates and we show that such predicates are decidable. Our main contribution is the implementation of a theorem prover capable of practically characterizing many commonly sought-after properties of k-automatic sequences. We showcase a panoply of results achieved using our method. We give new explicit descriptions of the recurrence and appearance functions of a list of well-known k-automatic sequences. We define a related function, called the condensation function, and give explicit descriptions for it as well. We re-affirm known results on the critical exponent of some sequences and determine it for others where it was previously unknown. On the more theoretical side, we show that the subword complexity p(n) of k-automatic sequences is k-synchronized, i.e., the language of pairs (n, p(n)) (expressed in base k) is accepted by an automaton. Furthermore, we prove that the Lyndon factorization of k-automatic sequences is also k-automatic and explicitly compute the factorization for several sequences. Finally, we show that while the number of unbordered factors of length n is not k-synchronized, it is k-regular.

In 1912 Axel Thue sparked the study of combinatorics on words when he showed that the Thue-Morse sequence contains no overlaps, that is, factors of the form ayaya. Since then many interesting properties of sequences began to be discovered and studied. In this thesis, we consider a class of infinite sequences generated by automata, called the k-automatic sequences. In particular, we present a logical theory in which many properties of k-automatic sequences can be expressed as predicates and we show that such predicates are decidable. Our main contribution is the implementation of a theorem prover capable of practically characterizing many commonly sought-after properties of k-automatic sequences. We showcase a panoply of results achieved using our method. We give new explicit descriptions of the recurrence and appearance functions of a list of well-known k-automatic sequences. We define a related function, called the condensation function, and give explicit descriptions for it as well. We re-affirm known results on the critical exponent of some sequences and determine it for others where it was previously unknown. On the more theoretical side, we show that the subword complexity p(n) of k-automatic sequences is k-synchronized, i.e., the language of pairs (n, p(n)) (expressed in base k) is accepted by an automaton. Furthermore, we prove that the Lyndon factorization of k-automatic sequences is also k-automatic and explicitly compute the factorization for several sequences. Finally, we show that while the number of unbordered factors of length n is not k-synchronized, it is k-regular.

Šiame darbe mes apžvelgėme modalumo logiką S4 bei kvantorinę modalumo logiką S4. Taip pat jų taisykles, aksiomas ir naudojamus skaičiavimus. Pateikėme kelias sekvencijų išvedimo pavyzdžių. Taip pat, apžvelgėme kai kurių, atskirų šių logikų klasių išsprendžiamumą. Taipogi šiame darbe buvo nagrinėjama labai įdomi tema – išsprendžiamumo klasių formavimas, naudojantis formulių transformavimų į klasikinę predikatų logiką. / Logic is the branch of mathematics that deals with the formal principles, methods and criteria of validity of inference, reasoning and knowledge. Logic is concerned with what is true and how we can know whether something is true. This involves the formalization of logical arguments and proofs in terms of symbols representing propositions and logical connectives. The goal of this work is to learn more about modal logic S4 and to consider some it decidable classes of formulas. It’s important, because decidable classes helps the substantiation of different formulas. In this work we will consider the formulas of modal logic without functional symbols.

Automated deduction procedures for modal logics, and related decidable fragments of first-order logic, are used in many real-world applications. A popular way of obtaining decision procedures for these logics is to base them on semantic tableau calculi. We focus on calculi that use unification, instead of the more widely employed approach of generating ground instantiations over the course of a derivation. The most common type of tableaux with unification are so-called free-variable tableaux, where variables are treated as global to the entire tableau. A long-standing open problem for procedures based on free-variable tableaux is how to ensure fairness, in the sense that "equivalent" applications of the closure rule are prevented from being done over and over again. Some solutions such as using depth-first iterative deepening are known, but those are unnecessary in theory, and not very efficient in practice. This is a main reason why there are hardly any decision procedures for modal logics based on free-variable tableaux. In this thesis, we review existing work on incorporating unification into first-order and modal tableau procedures, show how the closure fairness problem arises, and discuss existing solutions to it. For the first-order case, we outline a calculus which addresses the closure fairness problem. As opposed to free-variable tableaux, closure fairness is much easier to achieve in disconnection tableaux and similar clausal calculi. We therefore focus on using clausal first-order tableau calculi for decidable classes, in particular the two-variable fragment. Using the so-called unrestricted blocking mechanism for enforcing termination, we present the first ground tableau decision procedure for this fragment. Even for such a ground calculus, guaranteeing that depth-first terminations terminate is highly non-trivial. We parametrise our procedure by a so-called lookahead amount, and prove that this parameter is crucial for determining whether depth-first derivations terminate or not. Extending these ideas to tableaux with unification, we specify a preliminary disconnection tableau procedure which uses a non-grounding version of the unrestricted blocking rule.

In this thesis, we study advanced reasoning about dynamical systems in a logical framework -- the situation calculus. In particular, we consider promoting the efficiency of reasoning about action in the situation calculus from three different aspects. First, we propose a modified situation calculus based on the two-variable predicate logic with counting quantifiers. We show that solving the projection and executability problems via regression in such language are decidable. We prove that generally these two problems are co-NExpTime-complete in the modified language. We also consider restricting the format of regressable formulas and basic action theories (BATs) further to gain better computational complexity for reasoning about action via regression. We mention possible applications to formalization of Semantic Web services. Then, we propose a hierarchical representation of actions based on the situation calculus to facilitate development, maintenance and elaboration of very large taxonomies of actions. We show that our axioms can be more succinct, while still using an extended regression operator to solve the projection problem. Moreover, such representation has significant computational advantages. For taxonomies of actions that can be represented as finitely branching trees, the regression operator can sometimes work exponentially faster with our theories than it works with the BATs current situation calculus. We also propose a general guideline on how a taxonomy of actions can be constructed from the given set of effect axioms. Finally, we extend the current situation calculus with the order-sorted logic. In the new formalism, we add sort theories to the usual initial theories to describe taxonomies of objects. We then investigate what is the well-sortness for BATs under such framework. We consider extending the current regression operator with well-sortness checking and unification techniques. With the modified regression, we gain computational efficiency by terminating the regression earlier when reasoning tasks are ill-sorted and by reducing the search spaces for well-sorted objects. We also study that the connection between the order-sorted situation calculus and the current situation calculus.

In this thesis, we study advanced reasoning about dynamical systems in a logical framework -- the situation calculus. In particular, we consider promoting the efficiency of reasoning about action in the situation calculus from three different aspects. First, we propose a modified situation calculus based on the two-variable predicate logic with counting quantifiers. We show that solving the projection and executability problems via regression in such language are decidable. We prove that generally these two problems are co-NExpTime-complete in the modified language. We also consider restricting the format of regressable formulas and basic action theories (BATs) further to gain better computational complexity for reasoning about action via regression. We mention possible applications to formalization of Semantic Web services. Then, we propose a hierarchical representation of actions based on the situation calculus to facilitate development, maintenance and elaboration of very large taxonomies of actions. We show that our axioms can be more succinct, while still using an extended regression operator to solve the projection problem. Moreover, such representation has significant computational advantages. For taxonomies of actions that can be represented as finitely branching trees, the regression operator can sometimes work exponentially faster with our theories than it works with the BATs current situation calculus. We also propose a general guideline on how a taxonomy of actions can be constructed from the given set of effect axioms. Finally, we extend the current situation calculus with the order-sorted logic. In the new formalism, we add sort theories to the usual initial theories to describe taxonomies of objects. We then investigate what is the well-sortness for BATs under such framework. We consider extending the current regression operator with well-sortness checking and unification techniques. With the modified regression, we gain computational efficiency by terminating the regression earlier when reasoning tasks are ill-sorted and by reducing the search spaces for well-sorted objects. We also study that the connection between the order-sorted situation calculus and the current situation calculus.