Abstract: Publication date: June 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 105Author(s): Sándor Vágvölgyi We show second-order decidability results on recognizable tree languages and one-pass reduction sequences with special term rewriting systems. For some classes of term rewriting systems the second-order IO one-pass inclusion problem, the second-order IO one-pass reachability problem, and the IO and OI one-pass common ancestor problems are decidable.
Abstract: Publication date: June 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 105Author(s): Cosimo Laneve, Michael Lienhardt, Ka I Pun, Guillermo Román-Díez This paper proposes a technique for estimating the computational time of programs in an actor model, which is intended to serve as a compiler target of a wide variety of actor-based programming languages. We define a compositional translation function returning cost equations, which are fed to an automatic off-the-shelf solver for obtaining the time bounds. Our approach is based on a new notion of synchronization sets, which captures possible difficult synchronization patterns between actors and helps make the analysis efficient and precise. The approach is proven to correctly over-approximate the worst computational time of an actor model of concurrent programs. Our technique is complemented by a prototype analyzer that returns upper bound of costs for the actor model.
Abstract: Publication date: June 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 105Author(s): L.S. Jensen, I. Kaufmann, K.G. Larsen, S.M. Nielsen, J. Srba We investigate the open synthesis problem in a quantitative game theoretic setting where the system model is annotated with multiple nonnegative weights representing quantitative resources such as energy, discrete time or cost. We consider system specifications expressed in the branching time logic CTL extended with bounds on resources. As our first contribution, we show that the model checking problem for the full logic is undecidable with already three weights. By restricting the bounds to constant upper or lower-bounds on the individual weights, we demonstrate that the problem becomes decidable and that the model checking problem is PSPACE-complete. As a second contribution, we show that by imposing upper-bounds on the temporal operators and assuming that the cost converges over infinite runs, the synthesis problem is also decidable. Finally, we provide an on-the-fly algorithm for the synthesis problem on an unrestricted model for a reachability fragment of the logic and we prove EXPTIME-completeness of the synthesis problem.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Radosław Klimek This work relates to the automatic generation of logical specifications extracted directly from workflow-oriented behavioural models of software. The aim is to present a unified framework, which gives formal foundations and an algorithm for the logical specification generation process, allowing for further implementation works. Logical specifications are considered as sets of temporal logic formulas. The extraction process relies on the assumption that the entire developed model is structured purely by predefined workflow patterns. We are proposing a method to automatically transform behavioural models into logical specifications. This pattern-based feature-compositional approach, which we have denoted as ΠC, allows us to preserve the logical satisfiability, whilst guaranteeing expressiveness and naturality. Applying these concepts with user-friendly notations enables us to form a stronger link between the benefits of possessing behavioural model logical specifications, obtained automatically and on demand, with the ability to routinely analyse the developed software models in a logical style.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Mauricio Toro Various formal languages have been proposed in the literature for the individual-based modelling of ecological systems. These languages differ in their treatment of time and space. Each modelling language offers a distinct view and techniques for analyzing systems. Most of the languages are based on process calculi or P systems. In this article, we present a general overview of the existing modelling languages based on process calculi. We also discuss, briefly, other approaches such as P systems, cellular automata and Petri nets. Finally, we show advantages and disadvantages of these modelling languages and we propose some future research directions.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Bernhard Möller Time Geography is a framework for describing reachable points in a (static) spatio-temporal environment. While originally devised to facilitate reasoning about an individual's or a population's living conditions, it was later adapted to many other applications. A wayfinder is an entity that moves through a space-time continuum with possible obstacles. We show how to model the pertinent notions in relational algebra (and, more abstractly, in modal semirings) with box and diamond operators. Admissible or undesired regions can be described as Boolean combinations of primitive regions such as the set of all points reachable by forward or backward movement from a given region or starting point. To derive results about the region blocked by the union of two regions we introduce an abstract algebraic view of coordinates that is largely independent of dimensional and metric aspects and thus very general. Moreover, the approach lends itself quite well to machine-supported proofs.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Eva Graversen, Iain Phillips, Nobuko Yoshida We study categories for reversible computing, focussing on reversible forms of event structures. Event structures are a well-established model of true concurrency. There exist a number of forms of event structures, including prime event structures, asymmetric event structures, and general event structures. More recently, reversible forms of these types of event structure have been defined. We formulate corresponding categories and functors between them. We show that products and coproducts exist in many cases.We define stable reversible general event structures and stable configuration systems, and we obtain an isomorphism between the subcategory of the former in normal form and the finitely enabled subcategory of the latter.In most work on reversible computing, including reversible process calculi, a causality condition is posited, meaning that the cause of an event may not be reversed before the event itself. Since reversible event structures are not assumed to be causal in general, we also define causal subcategories of these event structures.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Thomas Troels Hildebrandt, Christian Johansen, Håkon Normann We give the first non-interleaving early operational semantics for the pi-calculus which generalises the standard interleaving semantics and unfolds to the stable model of prime event structures. Our starting point is the non-interleaving semantics given for CCS by Mukund and Nielsen, where the so-called structural (prefixing or subject) causality and events are defined from a notion of locations derived from the syntactic structure of the process terms. We conservatively extend this semantics with a notion of extruder histories, from which we infer the so-called link (name or object) causality and events introduced by the dynamic communication topology of the pi-calculus. We prove that the semantics generalises both the standard interleaving early semantics for the pi-calculus and the non-interleaving semantics for CCS. In particular, it gives rise to a labelled asynchronous transition system unfolding to prime event structures.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Alceste Scalas, Nobuko Yoshida This paper proves the soundness and completeness, together referred to as preciseness, of the subtyping relation for a synchronous multiparty session calculus.We address preciseness from operational and denotational viewpoints. The operational preciseness has been recently developed with respect to type safety, i.e., the safe replacement of a process of a smaller type in a context where a process of a bigger type is expected. The denotational preciseness is based on the denotation of a type: a mathematical object describing the meaning of the type, in accordance with the denotations of other expressions from the language.The main technical contribution of this paper is a novel proof strategy for the operational completeness of subtyping. We develop the notion of characteristic global type of a session type T, which describes a deadlock-free circular communication protocol involving all participants appearing in T. We prove operational completeness by showing that, if we place a process not conforming to a subtype of T in a context that matches the characteristic global type of T, then we obtain a deadlock. The denotational preciseness is proved as a corollary of the operational preciseness.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Andrzej S. Murawski, Nikos Tzevelekos Linearisability is a central notion for verifying concurrent libraries: a library is proven correct if its operational history can be rearranged into a sequential one that satisfies a given specification. Until now, linearisability has been examined for libraries in which method arguments and method results were of ground type. In this paper we extend linearisability to the general higher-order setting, where methods of arbitrary type can be passed as arguments and returned as values, and establish its soundness.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Hubert Garavel Petri nets can express concurrency and nondeterminism but neither locality nor hierarchy. This article presents an extension of Petri nets, in which places can be grouped into so-called “units” expressing sequential components. Units can be recursively nested to reflect both the concurrent and hierarchical nature of complex systems. This model called NUPN (Nested-Unit Petri Nets) was originally developed for translating process calculi to Petri nets, but later found also useful beyond this setting. It allows significant savings in the memory representation of markings for both explicit-state and symbolic verification. Thirteen software tools already implement the NUPN model, which has also been adopted for the benchmarks of the Model Checking Contest (MCC) and the parallel problems of the Rigorous Examination of Reactive Systems (RERS) challenges.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Rui Wang, Lars Michael Kristensen, Hein Meling, Volker Stolz Implementing test suites for distributed software systems is a complex and time-consuming task due to the number of test cases that need to be considered in order to obtain high coverage. We show how a formal Coloured Petri Net model can be used to automatically generate a suite of test cases for the Paxos distributed consensus protocol. The test cases cover both normal operation of the protocol as well as failure injection. To evaluate our model-based testing approach, we have implemented the Paxos protocol in the Go programming language using the quorum abstractions provided by the Gorums framework. Our experimental evaluation shows that we obtain high code coverage for our Paxos implementation using the automatically generated test cases.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Stephan Mennicke, Tobias Prehn Fairness assumptions are commonly used to filter system behaviors, thereby distinguishing between realistic and unrealistic executions. This allows for key arguments in correctness proofs of distributed systems, which would not be possible otherwise. Our first contribution is an equivalence spectrum in which fairness assumptions are preserved. Although the identified equivalences allow for reasoning about correctness incorporating fairness assumptions, this does not necessarily allow for the lifting of arguments from sequential processes to parallel compositions employing arbitrary synchronization mechanisms. Our second contribution is, therefore, an analysis of parallel composition operators and their synchronization mechanisms in this respect.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Frank Drewes, Berthold Hoffmann, Mark Minas Hyperedge replacement (HR) grammars can generate NP-complete graph languages, which makes parsing hard even for fixed HR languages. Therefore, we study predictive shift-reduce (PSR) parsing that yields efficient parsers for a subclass of HR grammars, by generalizing the concepts of SLR(1) string parsing to graphs. We formalize the construction of PSR parsers and show that it is correct. PSR parsers run in linear space and time, and are more efficient than the predictive top-down (PTD ) parsers recently developed by the authors.
Abstract: Publication date: April 2019Source: Journal of Logical and Algebraic Methods in Programming, Volume 104Author(s): Andrea Corradini, Barbara König, Dennis Nolte We investigate three formalisms for specifying graph languages, i.e. sets of graphs, based on type graphs. First, we are interested in (pure) type graphs, where the corresponding language consists of all graphs that can be mapped homomorphically to a given type graph. In this context, we also study languages specified by restriction graphs and their relation to type graphs. Second, we extend this basic approach to a type graph logic and, third, to type graphs with annotations. We present decidability results and closure properties for each of the formalisms.
Abstract: Publication date: Available online 21 March 2019Source: Journal of Logical and Algebraic Methods in ProgrammingAuthor(s): Gerco van Heerdt, Joshua Moerman, Matteo Sammartino, Alexandra Silva The classical subset construction for non-deterministic automata can be generalized to other side-effects captured by a monad. The key insight is that both the state space of the determinized automaton and its semantics—languages over an alphabet—have a common algebraic structure: they are Eilenberg-Moore algebras for the powersetgen monad. In this paper we study the reverse question to determinization. We will present a construction to associate succinct automata to languages based on different algebraic structures. For instance, for classical regular languages the construction will transform a deterministic automaton into a non-deterministic one, where the states represent the join-irreducibles of the language accepted by a (potentially) larger deterministic automaton. Other examples will yield alternating automata, automata with symmetries, CABA-structured automata, and weighted automata.
Abstract: Publication date: Available online 19 March 2019Source: Journal of Logical and Algebraic Methods in ProgrammingAuthor(s): Mahsa Varshosaz, Lars Luthmann, Paul Mohr, Malte Lochau, Mohammad Reza Mousavi Featured transition systems (FTSs) and modal transition systems (MTSs) are two of the most prominent and well-studied formalisms for modeling and analyzing behavioral variability as apparent in software product line engineering. On one hand, it is well-known that for finite behavior FTSs are strictly more expressive than MTSs, essentially due to the inability of MTSs to express logically constrained behavioral variability such as persistently exclusive behaviors. On the other hand, MTSs enjoy many desirable formal properties such as compositionality of semantic refinement and parallel composition. In order to finally consolidate the two formalisms for variability modeling, we establish a rigorous connection between FTSs and MTSs by means of an encoding of one FTS into an equivalent set of multiple MTSs. To this end, we split the structure of an FTS into several MTSs whenever it is necessary to denote exclusive choices that are not expressible in a single MTS. Moreover, extra care is taken when dealing with infinite behaviour: loops may have to be unrolled to accumulate FTS path constraints when encoding them into MTSs. We prove our encoding to be semantic-preserving (i.e., the resulting set of MTSs induces, up to bisimulation, the same set of derivable variants as their FTS counterpart) and to commute with modal refinement. We further give an algorithm to calculate a concise representation of a given FTS as a minimal set of MTSs. Finally, we present experimental results gained from applying a tool implementation of our approach to a collection of case studies.
Abstract: Publication date: Available online 18 March 2019Source: Journal of Logical and Algebraic Methods in ProgrammingAuthor(s): Philipp Haller, Heather Miller Asynchronous programming has gained in importance, not only due to hardware developments like multi-core processors, but also due to pervasive asynchronicity in client-side Web programming and large-scale Web applications. However, asynchronous programming is challenging. For example, control-flow management and error handling are much more complex in an asynchronous than a synchronous context. Programming with asynchronous event streams is especially difficult: expressing asynchronous stream producers and consumers requires explicit state machines in continuation-passing style when using widely-used languages like Java.In order to address this challenge, recent language designs like Google's Dart introduce asynchronous generators which allow expressing complex asynchronous programs in a familiar blocking style while using efficient non-blocking concurrency control under the hood. However, several issues remain unresolved, including the integration of analogous constructs into statically-typed languages, and the formalization and proof of important correctness properties.This paper presents a design for asynchronous stream generators for Scala, thereby extending previous facilities for asynchronous programming in Scala from tasks/futures to asynchronous streams. We present a complete formalization of the programming model based on a reduction semantics and a static type system. Building on the formal model, we contribute a complete type soundness proof, as well as the proof of a subject reduction theorem which establishes that the programming model enforces an important state transition protocol for asynchronous streams.
Abstract: Publication date: Available online 19 January 2019Source: Journal of Logical and Algebraic Methods in ProgrammingAuthor(s): Tuba Yavuz In this paper we present a counter-example guided abstraction and approximation (CEGAAR) refinement technique for partial predicate abstraction, which combines predicate abstraction and fixpoint approximations for model checking infinite-state systems. The proposed approach incrementally considers growing sets of predicates for abstraction refinement. The novelty of the approach stems from recognizing source of the imprecision: abstraction or approximation. We use Craig interpolation to deal with imprecision due to abstraction. In the case of imprecision due to approximation, we delay application of the approximation. Our experimental results on a variety of models provide insights into effectiveness of partial predicate abstraction as well as refinement techniques in this context.
Abstract: Publication date: Available online 11 January 2019Source: Journal of Logical and Algebraic Methods in ProgrammingAuthor(s): Fernando Macías, Uwe Wolter, Adrian Rutle, Francisco Durán, Roberto Rodriguez-Echeverria The use of Domain-Specific Languages (DSLs) is a promising field for the development of tools tailored to specific problem spaces, effectively diminishing the complexity of hand-made software. With the goal of making models as precise, simple and reusable as possible, we augment DSLs with concepts from multilevel modelling, where the number of abstraction levels are not limited. This is particularly useful for DSL definitions with behaviour, whose concepts inherently belong to different levels of abstraction. Here, models can represent the state of the modelled system and evolve using model transformations. These transformations can benefit from a multilevel setting, becoming a precise and reusable definition of the semantics for behavioural modelling languages. We present in this paper the concept of Multilevel Coupled Model Transformations, together with examples, formal definitions and tools to assess their conceptual soundness and practical value.
Abstract: Publication date: Available online 27 November 2018Source: Journal of Logical and Algebraic Methods in ProgrammingAuthor(s): Daniel Kernberger, Martin Lange We consider hybridisations of the full branching time logic CTL⁎ and its prominent fragments CTL, CTL+ and FCTL+ through the addition of nominals, binders and jumps. We formally define three types of hybridisations by restricting the interplay between hybrid operators and path formulas contrary to previous proposals in the literature which ignored potential problems with a formal semantics. We then investigate the model checking problem for these logics obtaining expression complexities from PSpace -completeness to non-elementary decidability and data complexities ranging from NLogSpace to PSpace. Lastly, we identify a family of fragments of these hybrid logics, called the bounded fragments, that (in some cases) have the same model checking complexity as their non-hybrid counterparts.
Abstract: Publication date: Available online 22 November 2018Source: Journal of Logical and Algebraic Methods in ProgrammingAuthor(s): S. Akshay, Loïc Hélouët, Ramchandra Phawade Time Petri nets (TPNs) are a classical extension of Petri nets with timing constraints attached to transitions, for which most verification problems are undecidable. We consider TPNs under a strong semantics with multiple enablings of transitions. We focus on a structural subclass of unbounded TPNs, where the underlying untimed net is free choice, and show that it enjoys nice properties in the timed setting under a multi-enabling semantics. In particular, we show that the questions of firability (whether a chosen transition can fire), and termination (whether the net has a non-terminating run) are decidable for this class. Next, we consider the problem of robustness under guard enlargement and guard shrinking, i.e., whether a given property is preserved even if the system is implemented on an architecture with imprecise time measurement. For unbounded free choice TPNs with a multi-enabling semantics, we show decidability of robustness of firability and of termination under both guard enlargement and shrinking.
Hybrid journal (It can contain Open Access articles)
[3201 journals]
