A Query Language for Workflow Logs

A business process (workflow) is an assembly of tasks to accomplish a business goal. Real-world workflow models often demanded to change due to new laws and policies, changes in the environment, and so on. To understand the inner workings of a business process to facilitate changes, workflow logs have the potential to enable inspecting, monitoring, diagnosing, analyzing, and improving the design of a complex workflow. Querying workflow logs, however, is still mostly an ad hoc practice by workflow managers. In this article, we focus on the problem of querying workflow log concerning both control flow and dataflow properties. We develop a query language based on “incident patterns” to allow the user to directly query workflow logs instead of having to transform such queries into database operations. We provide the formal semantics and a query evaluation algorithm of our language. By deriving an accurate cost model, we develop an optimization mechanism to accelerate query evaluation. Our experiment results demonstrate the effectiveness of the optimization and achieves up to 50× speedup over an adaption of existing evaluation method.

Reasoning about “reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recursion

Metareasoning can be achieved in probabilistic programming languages (PPLs) using agent models that recursively nest inference queries inside inference queries. However, the semantics of this powerful, reflection-like language feature has defied an operational treatment, much less reasoning principles for contextual equivalence. We give formal semantics to a core PPL with continuous distributions, scoring, general recursion, and nested queries. Unlike prior work, the presence of nested queries and general recursion makes it impossible to stratify the definition of a sampling-based operational semantics and that of a measure-theoretic semantics—the two semantics must be defined mutually recursively. A key yet challenging property we establish is that probabilistic programs have well-defined meanings: limits exist for the step-indexed measures they induce. Beyond a semantics, we offer relational reasoning principles for probabilistic programs making nested queries. We construct a step-indexed, biorthogonal logical-relations model. A soundness theorem establishes that logical relatedness implies contextual equivalence. We demonstrate the usefulness of the reasoning principles by proving novel equivalences of practical relevance—in particular, game-playing and decisionmaking agents. We mechanize our technical developments leading to the soundness proof using the Coq proof assistant. Nested queries are an important yet theoretically underdeveloped linguistic feature in PPLs; we are first to give them semantics in the presence of general recursion and to provide them with sound reasoning principles for contextual equivalence.

Solving string constraints with Regex-dependent functions through transducers with priorities and variables

Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provides such support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is generally undecidable, we show that our approach is complete for the so-called straight-line fragment. We evaluate the performance of our string solver on over 195000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods (via symbolic execution) in both precision and efficiency.

The cognitive mechanisms involved in the “DEGREE ADVERB + PROPER NAME” construction: Evaluating proposals from Construction Grammar and Formal Semantics

There are broad disagreements between existing models regarding the mental representations and processes involved in the "DEGREE ADVERB + PROPER NAME" construction, including disagreements regarding the semantics of the degree device, the category status of the proper name, the construction’s expressed meaning and its (non-)compositionality, and, crucially, the operation that holds between the degree device and the proper name. Our corpus-based investigation into two competing models from Construction Grammar and Formal Semantics shows that these models collectively make useful contributions to the scientific understanding of this construction, but neither is empirically adequate. Most importantly, we find that the construction participates in several non-predicted expressed meanings; multivariate analyses show that the three amenable to statistical analysis cluster with different semantic usage-features. We argue that the best way to account for the construction’s semantics-pragmatics is via a previously-dismissed cognitive mechanism: an enrichment-/strengthening-type operation whereby a pragmatically-supplied scale is added to the message.

Linguistic Accommodation

Accommodation is the process whereby a listener makes adjustments in response to behavior of the speaker. In the area of linguistics we might broadly label as theoretical pragmatics, within which we include much of formal semantics and philosophy of language, accommodation is the mechanism whereby hearers modify their representation of the conversational background so as to match assumptions that the speaker has made. The most pervasive type of accommodation involves presupposition, when a speaker takes some type of information for granted. Accommodation of presuppositions occurs when the listener adjusts their knowledge state in order to match the information that a speaker has presupposed. For example, if a speaker says, “I have to go pick up my sister from the airport,” there is a presupposition triggered that the speaker has a sister. If the listener is not already aware of the existence of the sister, they must accommodate this information by adjusting their information state accordingly. Two dominant approaches to modeling presupposition behavior have emerged in the past few decades, resulting in two broad understandings of accommodation. For a class of dynamic semantic theories, accommodation is a process that involves satisfaction in local contexts. On the other hand, a wave of research on presupposition as anaphora relies on a notion of accommodation as the creation of antecedents to enable anaphoric resolution that would otherwise fail. Within both understandings of accommodation, the particular mechanisms can also vary. Some accounts weigh the plausibility of material to be accommodated, some accounts weigh the alternative contexts within which material might be accommodated, and some weigh the amount of descriptive content contributed by the presupposition. Besides accommodation in theoretical pragmatics, a broader notion of accommodation is prominent in sociolinguistics, as well as further afield from linguistics in social psychology and anthropology. This notion includes not only the beliefs of the interlocutors, but also many other aspects of speech style and communicative behavior more generally. This literature primarily draws from communication accommodation theory (CAT), according to which a speaker adjusts their communicative behavior based on that of their interlocuter. Commonly, this adjustment involves mirroring, but interlocutors may also adjust to make differences salient rather than emphasizing similarity. While theoretical pragmatic and sociolinguistic accommodation are distinct notions with independent intellectual histories, presupposition accommodation can be seen as a special case of sociolinguistic accommodation. Both involve a hearer’s adjustment in response to a speaker. However, the former is more restrictive, concerning only adjustment to increase similarity, and only adjustment of aspects of what Lewis termed the conversational scoreboard, within which he includes the beliefs of the speaker and hearer.

Modelling Selectional Super-Flexibility

The selectional flexibility of some attitude verbs (e.g. know, realize, report) between declarative and interrogative complements has been the subject of much recent work in formal semantics. However, little attention has been paid to verbs (e.g. see, remember, observe) that embed an even wider variety of complements (incl. subject-controlled gerundive small clauses and concrete object-denoting DPs). Since the familiar types of some of these complements resist an embedding in the type for questions [= sets of propositions], these verbs challenge Theiler, Roelofsen & Aloni’s (2018) uniform interpretation strategy for the complements of responsive verbs. My paper answers this challenge by uniformly interpreting the different complements of selectionally super-flexible verbs like remember in a generalized type for questions, viz. as parametrized centered questions. It shows that the resulting semantics captures the intuitive entailment pattern of these verbs.

Qualitative Analysis of State/Event Fault Trees Based on Interface Automata

State/Event Fault Tree (SEFT) can be used for safety modeling and assessment. However, SEFT does not provide adequate semantics for analyzing the minimal scenarios leading to system failures. In this paper, we propose a novel qualitative analysis method for SEFT based on interface automata. Firstly, we propose the concept of guarded interface automata by adding guards on interface automata transitions. Based on this model, we can describe the triggers and guards of SEFT simultaneously. Then, a weak bisimilarity operation is defined to alleviate the state space explosion problem. Based on the proposed guarded interface automata and the weak bisimilarity operation, the semantics of SEFT can be precisely determined. After that, a qualitative analysis process is presented on the basis of the formal semantics of SEFT, and the analyzing result is the minimal cut sequence set representing the causes of system failures. Finally, a fire protection system case study is illustrated step by step to demonstrate the effectiveness of our method.

The visualization of a graph semantics of imperative languages

This work aims to present the software support for teaching in the field of formal semantics of imperative programming languages. The main part focuses on a software tool that provides a visual representation of the individual steps of the calculation in categorical semantics, which can also be referred to as graph semantics. The use of software tools in teaching to visually represent computational steps considerably facilitates understanding by students and can also serve as a good basis for supporting distance learning. Our program works in the standard form: after reading the correct user input, a visual representation of the meaning of the program is generated in the form of a category of states, which is displayed as an oriented graph. For better extensibility, the program is implemented as a web application.

Autotuning Parallel Programs by Model Checking

The paper presents a new approach to autotuning data-parallel programs. Autotuning is a search for optimal program settings which maximize its performance. The novelty of the approach lies in the use of the model checking method to find the optimal tuning parameters by the method of counterexamples. In our work, we abstract from specific programs and specific processors by defining their representative abstract patterns. Our method of counterexamples implements the following four steps. At the first step, an execution model of an abstract program on an abstract processor is described in the language of a model checking tool. At the second step, in the language of the model checking tool, we formulate the optimality property that depends on the constructed model. At the third step, we find the optimal values of the tuning parameters by using a counterexample constructed during the verification of the optimality property. In the fourth step, we extract the information about the tuning parameters from the counter-example for the optimal parameters. We apply this approach to autotuning parallel programs written in OpenCL, a popular modern language that extends the C language for programming both standard multi-core processors (CPUs) and massively parallel graphics processing units (GPUs). As a verification tool, we use the SPIN verifier and its model representation language Promela, whose formal semantics is good for modelling the execution of parallel programs on processors with different architectures.