Search

We show that the first-order logical theory of the binary overlap-free words (and, more generally, the ${\alpha}$-free words for rational ${\alpha}$, $2 < {\alpha} \leq 7/3$), is decidable. As a consequence, many results previously obtained about this class through tedious case- based proofs can now be proved "automatically", using a decision procedure.

We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formulas -- the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL., This manuscript is an extended and revised version of the publication with the same title that appeared at ESOP 2022 (https://doi.org/10.1007/978-3-030-44914-8_19). It is currently under review

A core part of the rehabilitation scheduling process consists of planning rehabilitation physiotherapy sessions for patients, by assigning proper operators to them in a certain time slot of a given day, taking into account several legal, medical and ethical requirements and optimizations, e.g., patient's preferences and operator's work balancing. Being able to efficiently solve such problem is of upmost importance, in particular after the COVID-19 pandemic that significantly increased rehabilitation's needs. In this paper, we present a two-phase solution to rehabilitation scheduling based on Answer Set Programming, which proved to be an effective tool for solving practical scheduling problems. We first present a general encoding, and then add domain specific optimizations. Results of experiments performed on both synthetic and real benchmarks, the latter provided by ICS Maugeri, show the effectiveness of our solution as well as the impact of our domain specific optimizations. Under consideration in Theory and Practice of Logic Programming (TPLP)., Under consideration in Theory and Practice of Logic Programming (TPLP)

We study expression learning problems with syntactic restrictions and introduce the class of finite-aspect checkable languages to characterize symbolic languages that admit decidable learning. The semantics of such languages can be defined using a bounded amount of auxiliary information that is independent of expression size but depends on a fixed structure over which evaluation occurs. We introduce a generic programming language for writing programs that evaluate expression syntax trees, and we give a meta-theorem that connects such programs for finite-aspect checkable languages to finite tree automata, which allows us to derive new decidable learning results and decision procedures for several expression learning problems by writing programs in the programming language.

We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut elimination and subformula property. Based on the same design, we introduce a variant of Lambek calculus with exponentials, aimed at capturing the controlled application of exchange and associativity. Properness (i.e., closure under uniform substitution of all parametric parts in rules) is the main technical novelty of the present proposal, allowing both for the smoothest proof of cut elimination and for the development of an overarching and modular treatment for a vast class of axiomatic extensions and expansions of intuitionistic, bi-intuitionistic, and classical linear logics with exponentials. Our proposal builds on an algebraic and order-theoretic analysis of linear logic and applies the guidelines of the multi-type methodology in the design of display calculi.

We provide a tutorial introduction to the algebraic graph rewriting formalism PBPO+. We show how PBPO+ can be obtained by composing a few simple building blocks, and model the reduction rules for binary decision diagrams as an example. Along the way, we comment on how alternative design decisions lead to related formalisms in the literature, such as DPO. We close with a detailed comparison with Bauderon's double pullback approach., Comment: In Proceedings TERMGRAPH 2022, arXiv:2303.14219

In this paper we revisit the topic of generalizing proof obligations in bit-level Property Directed Reachability (PDR). We provide a comprehensive study which (1) determines the complexity of the problem, (2) thoroughly analyzes limitations of existing methods, (3) introduces approaches to proof obligation generalization that have never been used in the context of PDR, (4) compares the strengths of different methods from a theoretical point of view, and (5) intensively evaluates the methods on various benchmarks from hardware model checking as well as from AI planning.

We present a framework for the formal meta-theory of lambda calculi in first-order syntax, with two sorts of names, one to represent both free and bound variables, and the other for constants, and by using Stoughton's multiple substitutions. On top of the framework we formalize Girard's proof of the Strong Normalization Theorem for both the simply-typed lambda calculus and System T. As to the latter, we also present a simplification of the original proof. The whole development has been machine-checked using the Agda system., Comment: In Proceedings LSFA 2022, arXiv:2303.12680

Critical systems require high reliability and are present in many domains. They are systems in which failure may result in financial damage or even loss of lives. Standard techniques of software engineering are not enough to ensure the absence of unacceptable failures and/or that critical requirements are fulfilled. Reo is a component-based modelling language that aims to provide a framework to build software based on existing pieces of software, which has been used in a wide variety of domains. Its formal semantics provides grounds to certify that systems based on Reo models satisfy specific requirements (i.e., absence of deadlocks). Current logical approaches for reasoning over Reo require the conversion of formal semantics into a logical framework. ReLo is a dynamic logic that naturally subsumes Reo's semantics. It provides a means to reason over Reo circuits. This work extends ReLo by introducing the iteration operator, and soundness and completeness proofs for its axiomatization., In Proceedings LSFA 2022, arXiv:2303.12680

In the paper we define three new complexity classes for Turing Machine undecidable problems inspired by the famous Cook/Levin’s NP-complete complexity class for intractable problems. These are U-complete (Universal complete), D-complete (Diagonalization complete) and H-complete (Hypercomputation complete) classes. In the paper, in the spirit of Cook/Levin/Karp, we started the population process of these new classes assigning several undecidable problems to them. We justify that some super-Turing models of computation, i.e., models going beyond Turing machines, are tremendously expressive and they allow to accept arbitrary languages over a given alphabet including those undecidable ones. We prove also that one of such super-Turing models of computation - the $-Calculus, designed as a tool for automatic problem solving and automatic programming, has also such tremendous expressiveness. We investigate also completeness of cost metrics and meta-search algorithms in $-calculus.

This work presents the system ANITA (Analytic Tableau Proof Assistant) developed for teaching analytic tableaux to computer science students. The tool is written in Python and can be used as a desktop application, or in a web platform. This paper describes the logical system of the tool, explains how the tool is used and compares it to several similar tools. ANITA has already been used in logic courses and an evaluation of the tool is presented., Comment: In Proceedings ThEdu'22, arXiv:2303.05360

The introduction of automated deduction systems in secondary schools face several bottlenecks. Beyond the problems related with the curricula and the teachers, the dissonance between the outcomes of the geometry automated theorem provers and the normal practice of conjecturing and proving in schools is a major barrier to a wider use of such tools in an educational environment. Since the early implementations of geometry automated theorem provers, applications of artificial intelligence methods, synthetic provers based on inference rules and using forward chaining reasoning are considered to be more suited for education proposes. Choosing an appropriate set of rules and an automated method that can use those rules is a major challenge. We discuss one such rule set and its implementation using the geometry deductive databases method (GDDM). The approach is tested using some chosen geometric conjectures that could be the goal of a 7th year class (approx. 12-year-old students). A lesson plan is presented, its goal is the introduction of formal demonstration of proving geometric theorems, trying to motivate students to that goal, In Proceedings ThEdu'22, arXiv:2303.05360

We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems and understanding of proofs in the higher-order logic of Isabelle/HOL in particular. The use of Isabelle enables almost automatic grading of large parts of the exam. We explain our approach through a number of example problems, and explain why we believe that each of the kinds of problems we have selected are adequate measures of our intended learning outcomes. Finally, we discuss our experiences using the approach for the exam of a course on automated reasoning and suggest potential future work., In Proceedings ThEdu'22, arXiv:2303.05360

One of the long-standing research problems on logic programming is to treat the cut predicate in a logical, high-level way. We argue that this problem can be solved by adopting linear logic and choice-disjunctive goal formulas of the form $G_0 \add G_1$ where $G_0, G_1$ are goals. These goals have the following intended semantics: $choose$ the true disjunct $G_i$ and execute $G_i$ where $i (= 0\ {\rm or}\ 1)$, while $discarding$ the unchosen disjunct. Note that only one goal can remain alive during execution. These goals thus allow us to specify mutually exclusive tasks in a high-level way., Comment: IEICE transaction on Information and Systems (to appear)

There exist two notions of equivalence of behavior between states of a Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The first one can be considered as an appropriate generalization to continuous spaces of Larsen and Skou's probabilistic bisimilarity, while the second one is characterized by a natural logic. C. Zhou expressed state bisimilarity as the greatest fixed point of an operator $\mathcal{O}$, and thus introduced an ordinal measure of the discrepancy between it and event bisimilarity. We call this ordinal the "Zhou ordinal" of $\mathbb{S}$, $\mathfrak{Z}(\mathbb{S})$. When $\mathfrak{Z}(\mathbb{S})=0$, $\mathbb{S}$ satisfies the Hennessy-Milner property. The second author proved the existence of an LMP $\mathbb{S}$ with $\mathfrak{Z}(\mathbb{S}) \geq 1$ and Zhou showed that there are LMPs having an infinite Zhou ordinal. In this paper we show that there are LMPs $\mathbb{S}$ over separable metrizable spaces having arbitrary large countable $\mathfrak{Z}(\mathbb{S})$ and that it is consistent with the axioms of $\mathit{ZFC}$ that there is such a process with an uncountable Zhou ordinal., v1: 19 pages. v2: role of the logic on Introduction, relation with previous constructions and 1 figure. Many minor corrections. v3: 20 pages. First item in former Lemma 30 was incorrect, but all the main results are still correct. Accepted at Review of Symbolic Logic. We are very grateful for the referee's useful suggestions and detailed reading

We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper- and lower-bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: we prove (1) that the reachability problem for COCA with global upper- and lower-bound tests is in NC 2 ; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is NP-complete for COCA with parametric counter updates and bound tests.

We develop a doubly-exponential decision procedure for the satisfiability problem of guarded separation logic -- a novel fragment of separation logic featuring user-supplied inductive predicates, Boolean connectives, and separating connectives, including restricted (guarded) versions of negation, magic wand, and septraction. Moreover, we show that dropping the guards for any of the above connectives leads to an undecidable fragment. We further apply our decision procedure to reason about entailments in the popular symbolic heap fragment of separation logic. In particular, we obtain a doubly-exponential decision procedure for entailments between (quantifier-free) symbolic heaps with inductive predicate definitions of bounded treewidth (SLIDbtw) - one of the most expressive decidable fragments of separation logic. Together with the recently shown 2ExpTime-hardness for entailments in said fragment, we conclude that the entailment problem for SLIDbtw is 2ExpTime-complete - thereby closing a previously open complexity gap., Substantial revision of v2

Relational verification encompasses information flow security, regression verification, translation validation for compilers, and more. Effective alignment of the programs and computations to be related facilitates use of simpler relational invariants and relational procedure specs, which in turn enables automation and modular reasoning. Alignment has been explored in terms of trace pairs, deductive rules of relational Hoare logics (RHL), and several forms of product automata. This article shows how a simple extension of Kleene Algebra with Tests (KAT), called BiKAT, subsumes prior formulations, including alignment witnesses for forall-exists properties, which brings to light new RHL-style rules for such properties. Alignments can be discovered algorithmically or devised manually but, in either case, their adequacy with respect to the original programs must be proved; an explicit algebra enables constructive proof by equational reasoning. Furthermore our approach inherits algorithmic benefits from existing KAT-based techniques and tools, which are applicable to a range of semantic models., Comment: v2 adds examples and an undecidability result; v3 has expository improvements (POPL version + appendix); v4 fixes the proof of Thm 4.3

This paper proposes a reconciliation of two different theories of information. The first, originally proposed in a lesser-known work by Claude Shannon, describes how the information content of channels can be described qualitatively, but still abstractly, in terms of information elements, i.e. equivalence relations over the data source domain. Shannon showed that these elements form a complete lattice, with the order expressing when one element is more informative than another. In the context of security and information flow this structure has been independently rediscovered several times, and used as a foundation for reasoning about information flow. The second theory of information is Dana Scott's domain theory, a mathematical framework for giving meaning to programs as continuous functions over a particular topology. Scott's partial ordering also represents when one element is more informative than another, but in the sense of computational progress, i.e. when one element is a more defined or evolved version of another. To give a satisfactory account of information flow in programs it is necessary to consider both theories together, to understand what information is conveyed by a program viewed as a channel (\`a la Shannon) but also by the definedness of its encoding (\`a la Scott). We combine these theories by defining the Lattice of Computable Information (LoCI), a lattice of preorders rather than equivalence relations. LoCI retains the rich lattice structure of Shannon's theory, filters out elements that do not make computational sense, and refines the remaining information elements to reflect how Scott's ordering captures the way that information is presented. We show how the new theory facilitates the first general definition of termination-insensitive information flow properties, a weakened form of information flow property commonly targeted by static program analyses., Comment: 30 pages; presented at the 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023), 15-21 January 2023

There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a power failure or a crash. Their correctness is typically stated in terms of \emph{durable linearizability} (DL), which requires that individual library operations appear to be executed atomically in a sequence consistent with the real-time order and, moreover, that recovering from a crash return a state corresponding to a prefix of that sequence. Sadly, however, there are hardly any formal DL proofs, and those that do exist cover the correctness of rather simple persistent algorithms on specific (simplified) persistency models. In response, we propose a general, powerful, modular, and incremental proof technique that can be used to guide the development and establish DL. Our technique is (1) general, in that it is not tied to a specific persistency and/or consistency model, (2) powerful, in that it can handle the most advanced persistent algorithms in the literature, (3) modular, in that it allows the reuse of an existing linearizability argument, and (4) incremental, in that the additional requirements for establishing DL depend on the complexity of the algorithm to be verified. We illustrate this technique on various versions of a persistent set, leading to the link-free set of Zuriel et al., 63 pages

Many modern autonomous systems, particularly multi-agent systems, are time-critical and need to be robust against timing uncertainties. Previous works have studied left and right time robustness of signal temporal logic specifications by considering time shifts in the predicates that are either only to the left or only to the right. We propose a combined notion of temporal robustness which simultaneously considers left and right time shifts. For instance, in a scenario where a robot plans a trajectory around a pedestrian, this combined notion can now capture uncertainty of the pedestrian arriving earlier or later than anticipated. We first derive desirable properties of this new notion with respect to left and right time shifts and then design control laws for linear systems that maximize temporal robustness using mixed-integer linear programming. Finally, we present two case studies to illustrate how the proposed temporal robustness accounts for timing uncertainties.

Partial combinatory algebras are algebraic structures that serve as generalized models of computation. In this paper, we study embeddings of pcas. In particular, we systematize the embeddings between relativizations of Kleene's models, of van Oosten's sequential computation model, and of Scott's graph model, showing that an embedding between two relativized models exists if and only if there exists a particular reduction between the oracles. We obtain a similar result for the lambda calculus, showing in particular that it cannot be embedded in Kleene's first model., Comment: 31 pages

Dedicated to Tony Hoare. In a paper published in 1972 Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data representations need not be mentioned in specifications that comprise the API of a module. Simulation: correctness of a new data representation and implementation can be established by proving simulation between the old and new implementations using a coupling relation defined on the encapsulated state. These results were formalized semantically and for a simple model of state, though the paper claimed this could be extended to encompass dynamically allocated objects. In recent years, progress has been made towards formalizing the claim, for simulation, though mainly in semantic developments. In this article, hiding and simulation are combined with the idea in Hoare's 1969 paper: a logic of programs. For an object-based language with dynamic allocation, we introduce a relational Hoare logic with stateful frame conditions that formalizes encapsulation, hiding of invariants, and couplings that relate two implementations. Relations and other assertions are expressed in first-order logic. Specifications can express a wide range of relational properties such as conditional equivalence and noninterference with declassification. The proof rules facilitate relational reasoning by means of convenient alignments and are shown sound with respect to a conventional operational semantics. A derived proof rule for equivalence of linked programs directly embodies representation independence. Applicability to representative examples is demonstrated using an SMT-based implementation., Comment: Vsn3: Revise exposition with more examples; add case study; add author; revise title, add index, minor changes throughout. Vsn4: Improved relational second order frame rule; revised and expanded examples and description of prototype; polish exposition. Vsn5: Rearrange some subsections, and other expository polishing. Version 6: add a couple of citations; version accepted to appear in ACM TOPLAS

Aiming at ontology-based data access to temporal data, we design two-dimensional temporal ontology and query languages by combining logics from the (extended) DL-Lite family with linear temporal logic LTL over discrete time (Z, 1, and FO(RPR) that admits relational primitive recursion. In terms of circuit complexity, FOE- and FO(RPR)-rewritability guarantee answering OMQs in uniform AC0 and NC1, respectively. We proceed in three steps. First, we define a hierarchy of 2D DL-Lite/LTL ontology languages and investigate the FO-rewritability of OMQs with atomic queries by constructing projections onto 1D LTL OMQs and employing recent results on the FO-rewritability of propositional LTL OMQs. As the projections involve deciding consistency of ontologies and data, we also consider the consistency problem for our languages. While the undecidability of consistency for 2D ontology languages with expressive Boolean role inclusions might be expected, we also show that, rather surprisingly, the restriction to Krom and Horn role inclusions leads to decidability (and ExpSpace-completeness), even if one admits full Booleans on concepts. As a final step, we lift some of the rewritability results for atomic OMQs to OMQs with expressive positive temporal instance queries. The lifting results are based on an in-depth study of the canonical models and only concern Horn ontologies., Accepted for JAIR

Cartesian differential categories come equipped with a differential combinator that formalizes the directional derivative from multivariable calculus. Cartesian differential categories provide a categorical semantics of the differential lambda-calculus and have also found applications in causal computation, incremental computation, game theory, differentiable programming, and machine learning. There has recently been a desire to provide a (coordinate-free) characterization of Jacobians and gradients in Cartesian differential categories. One's first attempt might be to consider Cartesian differential categories which are Cartesian closed, such as models of the differential lambda-calculus, and then take the curry of the derivative. Unfortunately, this approach excludes numerous important examples of Cartesian differential categories such as the category of real smooth functions. In this paper, we introduce linearly closed Cartesian differential categories, which are Cartesian differential categories that have an internal hom of linear maps, a bilinear evaluation map, and the ability to curry maps which are linear in their second argument. As such, the Jacobian of a map is defined as the curry of its derivative. Many well-known examples of Cartesian differential categories are linearly closed, such as, in particular, the category of real smooth functions. We also explain how a Cartesian closed differential category is linearly closed if and only if a certain linear idempotent on the internal hom splits. To define the gradient of a map, one must be able to define the transpose of the Jacobian, which can be done in a Cartesian reverse differential category. Thus, we define the gradient of a map to be the curry of its reverse derivative and show this equals the transpose of its Jacobian. We also explain how a linearly closed Cartesian reverse differential category is precisely a linearly closed Cartesian differential category with an appropriate notion of transpose., In Proceedings ACT 2021, arXiv:2211.01102

Native type systems are those in which type constructors are derived from term constructors, as well as the constructors of predicate logic and intuitionistic type theory. We present a method to construct native type systems for a broad class of languages, lambda-theories with equality, by embedding such a theory into the internal language of its topos of presheaves. Native types provide total specification of the structure of terms; and by internalizing transition systems, native type systems serve to reason about structure and behavior simultaneously. The construction is functorial, thereby providing a shared framework of higher-order reasoning for many languages, including programming languages., In Proceedings ACT 2021, arXiv:2211.01102

An old theorem of Ad\'amek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new version that works in constructive logic, using "inflationary" iteration over a notion of size that abstracts from limit ordinals just their transitive, directed and well-founded properties. Borrowing from Taylor's constructive treatment of ordinals, we show that sizes exist with upper bounds for any given signature of indexes. From this it follows that there is a rich class of endofunctors to which the new theorem applies, provided one admits a weak form of choice (WISC) due to Streicher, Moerdijk, van den Berg and Palmgren, and which is known to hold in the internal constructive logic of many kinds of topos., Comment: In Proceedings ACT 2021, arXiv:2211.01102

We demonstrate the first Recurrent Neural Network architecture for learning Signal Temporal Logic formulas, and present the first systematic comparison of formula inference methods. Legacy systems embed much expert knowledge which is not explicitly formalized. There is great interest in learning formal specifications that characterize the ideal behavior of such systems -- that is, formulas in temporal logic that are satisfied by the system's output signals. Such specifications can be used to better understand the system's behavior and improve design of its next iteration. Previous inference methods either assumed certain formula templates, or did a heuristic enumeration of all possible templates. This work proposes a neural network architecture that infers the formula structure via gradient descent, eliminating the need for imposing any specific templates. It combines learning of formula structure and parameters in one optimization. Through systematic comparison, we demonstrate that this method achieves similar or better mis-classification rates (MCR) than enumerative and lattice methods. We also observe that different formulas can achieve similar MCR, empirically demonstrating the under-determinism of the problem of temporal logic inference.

Approximate computing is an attractive paradigm for reducing the design complexity of error-resilient systems, therefore improving performance and saving power consumption. In this work, we propose a new two-level approximate logic synthesis method based on cube insertion and removal procedures. Experimental results have shown significant literal count and runtime reduction compared to the state-of-the-art approach. The method scalability is illustrated for a high error threshold over large benchmark circuits. The obtained solutions have presented a literal number reduction up to 38%, 56% and 93% with respect to an error rate of 1%, 3% and 5%, respectively., 5 Pages, submitted to IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

We introduce the probabilistic two-agent justification logic $\textsf {IPJ}$, a logic in which we can reason about agents that perform interactive proofs. In order to study the growth rate of the probabilities in $\textsf {IPJ}$, we present a new method of parametrizing $\textsf {IPJ}$ over certain negligible functions. Further, our approach leads to a new notion of zero-knowledge proofs.

We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. We give two reasons to do so. The first is proof-theoretical naturalness: the system consists of all and only the inference rules generated by the single, simple, linear scheme of the recently introduced subatomic logic. Thanks to this regularity, cuts are eliminated via a natural construction. The second reason is that the system generates efficient proofs. Indeed, we show that a certain class of tautologies due to Statman, which cannot have better than exponential cut-free proofs in the sequent calculus, have polynomial cut-free proofs in our system. We achieve this by using the same construction that we use for cut elimination. In summary, by expanding the language of propositional logic, we make its proof theory more regular and generate more proofs, some of which are very efficient. That design is made possible by considering atoms as superpositions of their truth values, which are connected by self-dual, non-commutative connectives. A proof can then be projected via each atom into two proofs, one for each truth value, without a need for cuts. Those projections are semantically natural and are at the heart of the constructions in this paper. To accommodate self-dual non-commutativity, we compose proofs in deep inference., Comment: To appear on ACM Transactions on Computational Logic

Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy’s merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. We contribute to answering this question in the simplified setting of the recursion-, relabelling-, and restriction-free fragment of CCS. We formulate three natural assumptions pertaining to the operational semantics of auxiliary operators and their relationship to parallel composition and prove that an auxiliary binary operator facilitating a finite axiomatisation of bisimilarity in the simplified setting cannot satisfy all three assumptions.

We present a novel approach for data set scaling based on scale-measures from formal concept analysis, i.e., continuous maps between closure systems, and derive a canonical representation. Moreover, we prove said scale-measures are lattice ordered with respect to the closure systems. This enables exploring the set of scale-measures through by the use of meet and join operations. Furthermore we show that the lattice of scale-measures is isomorphic to the lattice of sub-closure systems that arises from the original data. Finally, we provide another representation of scale-measures using propositional logic in terms of data set features. Our theoretical findings are discussed by means of examples., 19 pages, 6 figures

It is shown that a higher-dimensional automaton is hhp-bisimilar to the free symmetric HDA generated by it. Consequently, up to hereditary history-preserving bisimilarity, ordinary HDAs and symmetric HDAs are models of concurrency with the same expressive power.

Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding vacuity in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying the given constraints is a key enabler for the viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution, and can be very inefficient to produce legal scenarios of interest. We show how, given a set of constraints on the input scenarios succinctly defined by finite memory monitors, a data structure (scenario generator) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification., Comment: 14 pages. IEEE Transactions on Software Engineering, 2021

A recent strand of research in structural proof theory aims at exploring the notion of analytic calculi (i.e. those calculi that support general and modular proof-strategies for cut elimination), and at identifying classes of logics that can be captured in terms of these calculi. In this context, Wansing introduced the notion of proper display calculi as one possible design framework for proof calculi in which the analiticity desiderata are realized in a particularly transparent way. Recently, the theory of properly displayable logics (i.e. those logics that can be equivalently presented with some proper display calculus) has been developed in connection with generalized Sahlqvist theory (aka unified correspondence). Specifically, properly displayable logics have been syntactically characterized as those axiomatized by analytic inductive axioms, which can be equivalently and algorithmically transformed into analytic structural rules so that the resulting proper display calculi enjoy a set of basic properties: soundness, completeness, conservativity, cut elimination and subformula property. In this context, the proof that the given calculus is complete w.r.t. the original logic is usually carried out syntactically, i.e. by showing that a (cut free) derivation exists of each given axiom of the logic in the basic system to which the analytic structural rules algorithmically generated from the given axiom have been added. However, so far this proof strategy for syntactic completeness has been implemented on a case-by-case base, and not in general. In this paper, we address this gap by proving syntactic completeness for properly displayable logics in any normal (distributive) lattice expansion signature. Specifically, we show that for every analytic inductive axiom a cut free derivation can be effectively generated which has a specific shape, referred to as pre-normal form., arXiv admin note: text overlap with arXiv:1604.08822 by other authors

Event structures are fundamental models in concurrency theory, providing a representation of events in computation and of their relations, notably concurrency, conflict and causality. In this paper we present a theory of minimisation for event structures. Working in a class of event structures that generalises many stable event structure models in the literature (e.g., prime, asymmetric, flow and bundle event structures), we study a notion of behaviour-preserving quotient, referred to as a folding, taking (hereditary) history preserving bisimilarity as a reference behavioural equivalence. We show that for any event structure a folding producing a uniquely determined minimal quotient always exists. We observe that each event structure can be seen as the folding of a prime event structure, and that all foldings between general event structures arise from foldings of (suitably defined) corresponding prime event structures. This gives a special relevance to foldings in the class of prime event structures, which are studied in detail. We identify folding conditions for prime and asymmetric event structures, and show that also prime event structures always admit a unique minimal quotient (while this is not the case for various other event structure models).

Nominal automata are models for recognising languages over infinite alphabets, based on the algebraic notion of nominal set. Motivated by their use in automata theory, we show how to compute efficiently with nominal sets over the so-called total order symmetry, a variant which allows to compare alphabet letters for equality as well as their respective order. We develop an explicit finite representation of such nominal sets and basic constructions thereon. The approach is implemented as the library Ons (Ordered Nominal Sets), enabling programming with infinite sets. Returning to our motivation of nominal automata, we evaluate Ons in two applications: minimisation of automata and active automata learning. In both cases, Ons is competitive compared to existing implementations and outperforms them for certain classes of inputs.

This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the mu-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce a terminating tableau system for the logics we study, based on Kozen's tableau for the mu-calculus, and the one of Fitting and Massacci for modal logic., Comment: In Proceedings GandALF 2022, arXiv:2209.09333

Symbolic execution uses various algorithms (matching, (anti)unification), whose executions are parameters for proof object generation. This paper proposes a generic method for generating proof objects for such parameters. We present in detail how our method works for the case of antiunification. The approach is accompanied by an implementation prototype, including a proof object generator and a proof object checker. In order to investigate the size of the proof objects, we generate and check proof objects for inputs inspired from the K definitions of C and Java., Comment: In Proceedings FROM 2022, arXiv:2209.09208

We present an alternative translation from CCS to an extension of CSP based on m-among-n synchronisation (called CSPmn). This translation is correct up to strong bisimulation. Unlike the g-star renaming approach ([4]), this translation is not limited by replication (viz., recursion with no nested parallel composition). We show that m-among-n synchronisation can be implemented in CSP based on multiway synchronisation and renaming., Comment: In Proceedings EXPRESS/SOS 2022, arXiv:2208.14777

The Higher-Order $\Psi$-calculus framework (HO$\Psi$) is a generalisation of many first- and higher-order extensions of the $\pi$-calculus. It was proposed by Parrow et al. who showed that higher-order calculi such as HO$\pi$ and CHOCS can be expressed as HO$\Psi$-calculi. In this paper we present a generic type system for HO$\Psi$-calculi which extends previous work by H\"uttel on a generic type system for first-order $\Psi$-calculi. Our generic type system satisfies the usual property of subject reduction and can be instantiated to yield type systems for variants of HO{\pi}, including the type system for termination due to Demangeon et al. Moreover, we derive a type system for the $\rho$-calculus, a reflective higher-order calculus proposed by Meredith and Radestock. This establishes that our generic type system is richer than its predecessor, as the $\rho$-calculus cannot be encoded in the $\pi$-calculus in a way that satisfies standard criteria of encodability., Comment: In Proceedings EXPRESS/SOS 2022, arXiv:2208.14777

Reversing Petri nets (RPNs) have recently been proposed as a net-basedapproach to model causal and out-of-causal order reversibility. They are based on the notion of individual tokens that can be connected together via bonds. In this paper we extend RPNs by allowing multiple tokens of the same type to exist within a net based on the individual token interpretation of Petri nets. According to this interpretation, tokens of the same type are distinguished via their causal path. We develop a causal semantics of the model and we prove that the expressive power of RPNs with multiple tokens is equivalent to that of RPNs with single tokens by establishing an isomporphism between the Labelled Transition Systems (LTSs) capturing the reachable parts of the respective RPN models., In Proceedings EXPRESS/SOS 2022, arXiv:2208.14777

We prove that functions over the reals computable in polynomial time can be characterised using discrete ordinary differential equations (ODE), also known as finite differences. We also provide a characterisation of functions computable in polynomial space over the reals. In particular, this covers space complexity, while existing characterisations were only able to cover time complexity, and were restricted to functions over the integers. We prove furthermore that no artificial sign or test function is needed even for time complexity. At a technical level, this is obtained by proving that Turing machines can be simulated with analytic discrete ordinary differential equations. We believe this result opens the way to many applications, as it opens the possibility of programming with ODEs, with an underlying well-understood time and space complexity., arXiv admin note: text overlap with arXiv:2209.13404

ion is a key verification technique to improve scalability. However, its use for neural networks is so far extremely limited. Previous approaches for abstracting classification networks replace several neurons with one of them that is similar enough. We can classify the similarity as defined either syntactically (using quantities on the connections between neurons) or semantically (on the activation values of neurons for various inputs). Unfortunately, the previous approaches only achieve moderate reductions, when implemented at all. In this work, we provide a more flexible framework where a neuron can be replaced with a linear combination of other neurons, improving the reduction. We apply this approach both on syntactic and semantic abstractions, and implement and evaluate them experimentally. Further, we introduce a refinement method for our abstractions, allowing for finding a better balance between reduction and precision., Accepted at ATVA 2023

In multi-agent system design, a crucial aspect is to ensure robustness, meaning that for a coalition of agents A, small violations of adversarial assumptions only lead to small violations of A's goals. In this paper we introduce a logical framework for robust strategic reasoning about multi-agent systems. Specifically, inspired by recent works on robust temporal logics, we introduce and study rATL and rATL*, logics that extend the well-known Alternating-time Temporal Logic ATL and ATL* by means of an opportune multi-valued semantics for the strategy quantifiers and temporal operators. We study the model-checking and satisfiability problems for rATL and rATL* and show that dealing with robustness comes at no additional computational cost. Indeed, we show that these problems are PTime-complete and ExpTime-complete for rATL, respectively, while both are 2ExpTime-complete for rATL*.

There are many techniques and tools for termination of C programs, but up to now they were not very powerful for termination proofs of programs whose termination depends on recursive data structures like lists. We present the first approach that extends powerful techniques for termination analysis of C programs (with memory allocation and explicit pointer arithmetic) to lists., Presented at WST 2023, short version of arXiv:2305.12159

Underlying the theory of inferences, a primary task of logic is language analysis. Such a task can be understood as depending on a general theory of representation, taking as a starting point the idea that some entities (`` representations '') can present some entites (`` contents ''). We outline a theory of representation accounting for the capacity of representational systems to access universes that extend beyond an immediate presence. We define three logical properties that any adequate representational system should have: completeness, faithfulness, coherence. We show that logical laws are laws of representation. Finally, it appears that logic can be considered as the abstract theory of representation.

We consider the following problem: given $d \times d$ rational matrices $A_1, \ldots, A_k$ and a polyhedral cone $\mathcal{C} \subset \mathbb{R}^d$, decide whether there exists a non-zero vector whose orbit under multiplication by $A_1, \ldots, A_k$ is contained in $\mathcal{C}$. This problem can be interpreted as verifying the termination of multi-path while loops with linear updates and linear guard conditions. We show that this problem is decidable for commuting invertible matrices $A_1, \ldots, A_k$. The key to our decision procedure is to reinterpret this problem in a purely algebraic manner. Namely, we discover its connection with modules over the polynomial ring $\mathbb{R}[X_1, \ldots, X_k]$ as well as the polynomial semiring $\mathbb{R}_{\geq 0}[X_1, \ldots, X_k]$. The loop termination problem is then reduced to deciding whether a submodule of $\left(\mathbb{R}[X_1, \ldots, X_k]\right)^n$ contains a ``positive'' element., Comment: 6 pages

This paper deals with the problem of automatically and correctly controlling infinite-state reactive programs to achieve LTL goals. Applications include adapting a program to new requirements, or to repair bugs discovered in the original specification or program code. Existing approaches are able to solve this problem for safety and some reachability properties, but require an a priori template of the solution for more general properties. Fully automated approaches for full LTL exist, reducing the problem into successive finite LTL reactive synthesis problems in an abstraction-refinement loop. However, they do not terminate when the number of steps to be completed depends on unbounded variables. Our main insight is that safety abstractions of the program are not enough -- fairness properties are also essential to be able to decide many interesting problems, something missed by existing automated approaches. We thus go beyond the state-of-the-art to allow for automated reactive program control for full LTL, with automated discovery of the knowledge, including fairness, of the program needed to determine realisability. We further implement the approach in a tool, with an associated DSL for reactive programs, and illustrate the approach through several case studies.