1,721,750 research outputs found
Context-free Languages via Coalgebraic Trace Semantics
No full textWe show that, for functors with suitable mild restrictions, the initial algebra in the category of sets and functions gives rise to the final coalgebra in the (Kleisli) category of sets and relations. The finality principle thus obtained leads to the finite trace semantics of non-deterministic systems, which extends the trace semantics for coalgebras previously introduced by the second author. We demonstrate the use of our technical result by giving the first coalgebraic account on context-free grammars, where we obtain generated context-free languages via the finite trace semantics. Additionally, the constructions of both finite and possibly infinite parse trees are shown to be monads. Hence our extension of the application domain of coalgebras identifies several new mathematical constructions and structures
Antichain-based refinement checking benchmark using the mCRL2 toolset
No full textA set of benchmarks consisting of mCRL2 specifications that can be compared using the ltscompare tool of the mCRL2 toolset
On-The-Fly Solving for Symbolic Parity Games using the mCRL2 toolset
No full textThis artifact contains a set of mCRL2 specifications and formulas that are used to compare various on-the-fly solving techniques for symbolic parity games. The techniques are described in the paper "On-The-Fly Solving for Symbolic Parity Games" by Maurice Laveaux, Wieger Wesselink and Tim A.C. Willemse
Experiments for the paper "(Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems"
No full textThis archive contains files for experiments with quantifier elimination for parameterised Boolean equation systems, as described in the paper Thomas Neele, (Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems, in ARQNL 2022, CEUR-WS. Each folder contains an mCRL2 process specification, a modal mu-calculus formula and a bash script run.sh. To run the experiments, an installation of the mCRL2 tool set (version 202206.0 or newer) should be available in the PATH. Source code and binaries are available via https://mcrl2.org or https://github.com/mCRL2org/mCRL2. The run scripts automatically generate a linear process (LPS) and a PBES. The latter is used to compare three approaches: Not applying any constant elimination. Applying the standard constant elimination algorithm from the paper "Static Analysis Techniques for Parameterised Boolean Equation Systems" by Simona Orzan, Wieger Wesselink and Tim A. C. Willemse. Applying the quantifier analysis of the paper mentioned at the top. In case of the motivating example, the resulting PBES for each approach is printed to stdout. For the ABP and cache coherence examples, the size of the underlying BES (called structure graph in the tools) is printed
Experience report on developing the Front-end Client unit under the control of formal methods
Full text linkFormal methods are extensively being applied to the development of control software units, of highly sophisticated X-ray machines, at Philips Healthcare. One of the early units incorporating formal methods is the Front-end client (FEClient), which was developed under the control of formal technologies, supported by the Analytical Software Design (ASD) method. As a result, only eleven coding errors were detected during the construction of 28 thousands lines of code. Team members attribute the ultimate quality of the software to the rigor of the formal technologies supplied by the ASD method. In this paper we report about the experience of applying ASD to the development of the FEClient, and we show how formal methods substantially enhanced its quality. We also discuss the nature of the errors found during the construction of the unit
Revisiting timing in process algebra
No full textWe shortly review the framework of process algebras with timing presented by Baeten and Middelburg [Handbook of Process Algebra, Elsevier, 2001, Chapter 10]. In order to cover processes that are capable of performing certain actions at all points in some time interval, we add integration to the process algebra with continuous relative timing from this framework. This extension happens to reveal some points that are peculiar to relative timing. We go into these points.
The most flagrant point is that, unlike in case of absolute timing, discretization cannot be added to the extension without first adding a mechanism for parametric timing like initial abstraction
Guest editors’ introduction: Special issue on Probabilistic Techniques for the Design and Analysis of Systems
No full textNormalization of Infinite Terms
No full textWe investigate the property SN ¿8¿ being the natural concept related to termination when considering term rewriting applied to infinite terms. It turns out that this property can be fully characterized by a variant of monotone algebras equipped with a metric. A fruitful special case is obtained when the algebra is finite and the required metric properties are obtained for free. It turns out that the matrix method can be applied to find proofs of SN ¿8¿ based on these observations. In this way SN ¿8¿ can be proved fully automatically for some interesting examples related to combinatory logic
DFAs and PFAs with Long Shortest Synchronizing Word Length
No full textIt was conjectured by Černý in 1964, that a synchronizing DFA on n states always has a synchronizing word of length at most (n-1)2 and he gave a sequence of DFAs for which this bound is reached. Until now a full analysis of all DFAs reaching this bound was only given for n ≤ 4 and with bounds on the number of symbols for n ≤ 10 Here we give the full analysis for n ≤ 6 without bounds on the number of symbols. For PFAs on n ≤ 6 states we do a similar analysis as for DFAs and find the maximal shortest synchronizing word lengths, exceeding (n-1)2 for n = 4, 5, 6. For arbitrary n we use rewrite systems to construct a PFA on three symbols with exponential shortest synchronizing word length, giving significantly better bounds than earlier exponential constructions.We give a transformation of this PFAto a PFAon two symbols keeping exponential shortest synchronizing word length, yielding a better bound than applying a similar known transformation
- …
