194 research outputs found
Bond Anchorage of Pretensioned Frp Tendon At Force Release
No full textThe anchorage of fiber-reinforced plastic (FRP) tendons in pretensioned prestressed concrete (PC) members may cause the formation of cracks as a result of tendon wedge effect and mechanical interlocking during prestress force transfer. This paper presents experimental results obtained with a braided epoxy-impregnated aramid FRP tendon having a 16-mm nominal diameter and initial prestress force of 125.6 kN. Minimum concrete cover was 52 mm. End-zone reinforcement and tendon partial blanketing were used to determine their effect on concrete stress field intensity and on cracking due to prestress force transfer. It was found that steel stirrups do not prevent cracking, but they limit its propagation. A carbon FRP coil of small pitch inhibits crack formation, but the concrete tensile strain remains high. Partial blanketing is the most effective solution, causing only a limited increase in transfer length (approximately 20%). An analytical solution to the experiment was obtained by using the finite clement method, assuming a partly cracked elastic concrete ring model. This proved to be an effective tool for predicting the occurrence of cracks when using tendons of different size and/or initial prestress force
Generic Infinite Traces and Path-Based Coalgebraic Temporal Logics
No full textThis paper gives a general coalgebraic account of the notions of possibly infinite trace and possibly infinite execution in state-based, dynamical systems, by extending the generic theory of finite traces and executions developed by Hasuo and coauthors [8]. The systems we consider are modelled as coalgebras of endofunctors obtained as the composition of a computational type (e.g. nondeterministic or stochastic) with a general transition type. This generalises existing work by Jacobs [10] that only accounts for a nondeterministic computational type. We subsequently introduce path-based temporal (including fixpoint) logics for coalgebras of such endofunctors, whose semantics is based upon the notion of possibly infinite execution. Our approach instantiates to both nondeterministic and stochastic computations, yielding, in particular, path-based fixpoint logics in the style of CTL* for nondeterministic systems, as well as generalisations of the logic PCTL for probabilistic systems
Exemplifying parametric timed specifications over signals with bounded behavior
No full textSpecifying properties can be challenging work. In this paper, we propose an
automated approach to exemplify properties given in the form of automata
extended with timing constraints and timing parameters, and that can also
encode constraints over real-valued signals. That is, given such a
specification and given an admissible automaton for each signal, we output
concrete runs exemplifying real (or impossible) runs for this specification.
Specifically, our method takes as input a specification, and a set of
admissible behaviors, all given as a subclass of rectangular hybrid automata,
namely timed automata extended with arbitrary clock rates, signal constraints,
and timing parameters. Our method then generates concrete runs exemplifying the
specification.Comment: This is the author (and extended) version of the manuscript of the
same name published in the proceedings of the 14th NASA Formal Methods
Symposium (NFM 2022). This work is partially supported by ERATO HASUO
Metamathematics for Systems Design Project (No. JPMJER1603), JST and by the
ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015
Exploiting Adjoints in Property Directed Reachability Analysis
No full textWe formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley’s property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use the second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes
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
Generic Weakest Precondition Semantics from Monads Enriched with Order
No full textAbstract. We devise a generic framework where a weakest precondi-tion semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs’ recent identification of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: 1) different notions of modality (such as “may ” vs. “must”) are captured by Eilenberg-Moore algebras; 2) nested branching—like in games and in probabilistic systems with nondeterministic environments—is modularly modeled by a monad on the Eilenberg-Moore category of another.
Symbolic Monitoring against Specifications Parametric in Time and Data
No full textThis is the author version of the manuscript of the same name published in the proceedings of the 31st International Conference on Computer-Aided Verification (CAV 2019).International audienceMonitoring consists in deciding whether a log meets a given specification. In this work, we propose an automata-based formalism to monitor logs in the form of actions associated with time stamps and arbitrarily data values over infinite domains. Our formalism uses both timing parameters and data parameters, and is able to output answers symbolic in these parameters and in the log segments where the property is satisfied or violated. We implemented our approach in an ad-hoc prototype SyMon, and experiments show that its high expressive power still allows for efficient online monitoring
Offline timed pattern matching under uncertainty
No full textThis is the author version of the manuscript of the same name published in the proceedings of the 23rd International Conference on Engineering of Complex Computer Systems (ICECCS 2018).International audienceGiven a log and a specification, timed pattern matching aims at exhibiting for which start and end dates a specification holds on that log. For example, "a given action is always followed by another action before a given deadline". This problem has strong connections with monitoring real-time systems. We address here timed pattern matching in presence of an uncertain specification, i.e., that may contain timing parameters (e.g., the deadline can be uncertain or unknown). That is, we want to know for which start and end dates, and for what values of the deadline, this property holds. Or what is the minimum or maximum deadline (together with the corresponding start and end dates) for which this property holds. We propose here a framework for timed pattern matching based on parametric timed model checking. In contrast to most parametric timed problems, the solution is effectively computable, and we perform experiments using IMITATOR to show the applicability of our approach
Model-bounded monitoring of hybrid systems
No full textMonitoring of hybrid systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals, while real behaviors are continuous-time signals. To mitigate this problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use prior knowledge about the target system to prune interpolation candidates. Technically, we express such prior knowledge by linear hybrid automata (LHAs) -- the LHAs are called bounding models. We introduce a novel notion of monitored language of LHAs, and we reduce the monitoring problem to the membership problem of the monitored language. We present two partial algorithms -- one is via reduction to reachability in LHAs and the other is a direct one using polyhedra -- and show that these methods, and thus the proposed model-bounded monitoring scheme, are efficient and practically relevant.This is the author version of the manuscript of the same name published in the ACM Transactions on Cyber-Physical System
Parametric Timed Model Checking for Guaranteeing Timed Opacity
No full textThis is the author (and extended) version of the manuscript of the same name published in the proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019). This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002) and by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JSTInternational audienceInformation leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on the system execution time. We address the following problem: given a timed system, synthesize the execution times for which one cannot deduce whether the system performed some secret behavior. We solve this problem in the setting of timed automata (TAs). We first provide a general solution, and then extend the problem to parametric TAs, by synthesizing internal timings making the TA secure. We study decidability, devise algorithms, and show that our method can also apply to program analysis
- …
