BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Anna Ingolfsdottir

Anna Ingolfsdottir appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceSoftware EngineeringProgramming Languages

Catalog footprint

What is connected

7works
3topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

7 published item(s)

preprint2022arXiv

Axiomatizing recursion-free, regular monitors

Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al.$~$has specified monitors using a variation on the regular fragment of Milner's CCS and studied two trace-based notions of equivalence over monitors, namely verdict and $ω$-verdict equivalence. This article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of verdict and $ω$-verdict equivalence for closed and open terms over recursion-free monitors. It is also shown that verdict equivalence has no finite equational axiomatization over open monitors when the set of actions is finite and contains at least two actions.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

On the Axiomatisation of Branching Bisimulation Congruence over CCS

In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contribution, we show that, when the set of actions is finite, rooted branching bisimilarity has a finite equational basis over CCS enriched with the left merge and communication merge operators from ACP.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques

The PrePost (Pre- and Post-Deployment Verification Techniques) workshop aimed at bringing together researchers working in the field of computer-aided validation and verification to discuss the connections and interplay between pre- and post-deployment verification techniques. Examples of the topics covered by the workshop are the relationships between classic model checking and testing on the one hand and runtime verification and statistical model checking on the other, and between type systems that may be checked either statically or dynamically through techniques such as runtime monitoring.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Meta SOS - A Maude Based SOS Meta-Theory Framework

Meta SOS is a software framework designed to integrate the results from the meta-theory of structural operational semantics (SOS). These results include deriving semantic properties of language constructs just by syntactically analyzing their rule-based definition, as well as automatically deriving sound and ground-complete axiomatizations for languages, when considering a notion of behavioural equivalence. This paper describes the Meta SOS framework by blending aspects from the meta-theory of SOS, details on their implementation in Maude, and running examples.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Axiomatizing GSOS with Predicates

In this paper, we introduce an extension of the GSOS rule format with predicates such as termination, convergence and divergence. For this format we generalize the technique proposed by Aceto, Bloom and Vaandrager for the automatic generation of ground-complete axiomatizations of bisimilarity over GSOS systems. Our procedure is implemented in a tool that receives SOS specifications as input and derives the corresponding axiomatizations automatically. This paves the way to checking strong bisimilarity over process terms by means of theorem-proving techniques.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca

In this paper we propose an extension of the Rebeca language that can be used to model distributed and asynchronous systems with timing constraints. We provide the formal semantics of the language using Structural Operational Semantics, and show its expressiveness by means of examples. We developed a tool for automated translation from timed Rebeca to the Erlang language, which provides a first implementation of timed Rebeca. We can use the tool to set the parameters of timed Rebeca models, which represent the environment and component variables, and use McErlang to run multiple simulations for different settings. Timed Rebeca restricts the modeller to a pure asynchronous actor-based paradigm, where the structure of the model represents the service oriented architecture, while the computational model matches the network infrastructure. Simulation is shown to be an effective analysis support, specially where model checking faces almost immediate state explosion in an asynchronous setting.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages

This paper presents a bisimulation-based method for establishing the soundness of equations between terms constructed using operations whose semantics is specified by rules in the GSOS format of Bloom, Istrail and Meyer. The method is inspired by de Simone's FH-bisimilarity and uses transition rules as schematic transitions in a bisimulation-like relation between open terms. The soundness of the method is proven and examples showing its applicability are provided. The proposed bisimulation-based proof method is incomplete, but the article offers some completeness results for restricted classes of GSOS specifications.

0 citations0 reviewsNo code linkedOpen access