Wyniki wyszukiwania - BazTech

1

Monitorowanie geozagrożeń na terenach zurbanizowanych

Łukasik S.

Materiały Budowlane

|

2015

|

nr 11

24--26

PL

Skarpy nadrzeczne ze względu na walory przyrodnicze i kulturowe są atrakcyjnymi obszarami, na których obserwuje się nasiloną ekspansję inwestorów nowych obiektów. W celu ochrony terenów przed antropogeniczną dewastacją i naturalnymi procesami geodynamicznymi konieczne jest prognozowanie zachowania się skarp. Pierwszym obszarem, w przypadku którego prowadzono nowoczesny monitoring, była Skarpa Płocka (1982 – 2002). Korzystając z nabytych doświadczeń, w 2009 r. Zakład Geotechniki i Fundamentowania ITB opracował i zrealizował monitoring trzech obszarów Skarpy Warszawskiej na zlecenie Miasta Stołecznego Warszawy. W ramach projektu określono szczegółowe założenia do pomiarów przemieszczeń pionowych i poziomych systemu reperów ściennych, wgłębnych i inklinometrów w ilości ok. 500 szt. Wykonano 5 cykli pomiarowych, których wyniki zostały zgromadzone w specjalnie opracowanej bazie danych współpracującej z oprogramowaniem Oracle i ArcGis. System monitoringu stanowi ważny element zarządzania zasobami miejskimi, gwarantuje nadzór i kontrolę istniejących obiektów. Sukcesywne gromadzenie danych o przemieszczeniach skarpy jest istotnym elementem w pracach projektowych prowadzonych na rzecz zabezpieczenia zagrożonych odcinków.

EN

Riverside slopes zone are attractive new investment areas due to natural and cultural values. Intensified expansion of new building developers is currently observed. The slope behavior forecast is necessary to properly protect these areas from anthropogenic devastation and natural geodynamic processes. The first area covered with modern monitoring was Skarpa Płocka in 1982 – 2002. Using gained experience the Department of Geotechnics and Foundation in 2009, on City of Warsaw behalf, designed and executed the monitoring system for three areas of Skarpa Warszawska. The detailed guide lines for vertical and horizontal measurements of approx. 500 fix points were developed during the project. There were wall and earth plunge benchmarks installed as well as inclinometers. There were 5 measurement cycles to this day. The results were collected in special developed, cooperating with Oracle and ArcGis software database. The monitoring system is an important part of urban resources management. It guaranties land use planning supervision as well as existing facilities control.Successive collecting data on the slope movements is important element for design work undertaken for the protection of endangered areas.

2

Graded Alternating-Time Temporal Logic

Faella M., Napoli M., Parente M.

Fundamenta Informaticae

|

2011

|

Vol. 105, nr 1/2

189-210

EN

Recently, temporal logics such as μ-calculus and Computational Tree Logic, CTL, augmented with graded modalities have received attention from the scientific community, both from a theoretical side and from an applicative perspective. In both these settings, graded modalities enrich the universal and existential quantifiers with the capability to express the concept of at least k or all but k, for a non-negative integer k. Both μ-calculus and CTL naturally apply as specification languages for closed systems: in this paper, we study how graded modalities may affect specification languages for open systems. We extend the Alternating-time Temporal Logic (ATL) introduced by Alur et al., that is a derivative of CTL interpreted on game structures, rather than transition systems. We solve the model-checking problem in the concurrent and turn-based settings, proving its PTIME-completeness. We present, and compare with each other, two different semantics: the first seems suitable to off-line synthesis applicationswhile the secondmay find application in the verification of fault-tolerant controllers. We also study the case where players can only employ memoryless strategies, showing that also in this case the model-checking problem is in PTIME.

3

Coinductive axiomatization of recursive type equality and subtyping

Brandt M., Henglein F.

Fundamenta Informaticae

|

1998

|

Vol. 33, nr 4

309-338

EN

We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via simulation and bisimulation, respectively. The main novelty of the axiomatization is the fixpoint rule (or coinduction principle). It states that from A,Pý P one may deduce Aý P, where P is either a type equality t = t1 or type containment t